FormalConjecturesTest/Util/Linters/ExistsImplicationLinter.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

Imports (2)
  1. theorem this_doesnt_look_good line 29 source
  2. theorem even_worse line 39 source
  3. theorem this_is_fine sorry line 44 source

    depends on sorry (Lean reported 1 error(s) in this file) what this means

    Statement uses: Exists, Nat, Or, Ne, OfNat.ofNat, False

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.