FormalConjecturesTest/Util/Linters/StubLinter.lean

GitHub source file

9 declarations, 5 contain sorry, 1 declared as axioms

1. opaque MyOpaqueType line 31 source
2. axiom MyNewAxiom line 39 source

   extra axioms: MyNewAxiom (Lean reported 6 error(s) in this file) what this means

   Statement uses: Eq, Nat, OfNat.ofNat

   1 instances, coercions and auxiliary constants left out.

3. def MyDefSorry sorry line 47 source

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

   Statement uses: Nat

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

   1 instances, coercions and auxiliary constants left out.

4. def MyDefBySorry sorry line 55 source

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

   Statement uses: Nat

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

   1 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

5. def MyDefByAdmit line 63 source

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

   Statement uses: Nat

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

   1 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

6. def MyDefPattern sorry line 71 source

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

   Statement uses: Nat

   Proof uses: MyDefPattern.match_1, Unit, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   1 instances, coercions and auxiliary constants left out.

7. abbrev MyAbbrevSorry sorry line 79 source

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

   Statement uses: Nat

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

   1 instances, coercions and auxiliary constants left out.

8. def MyNormalType line 82 source
9. theorem MyTheoremWithSorry sorry line 85 source

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

   Statement uses: Eq, Nat, OfNat.ofNat

   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.