FormalConjecturesTest/Util/Answer.lean

GitHub source file

7 declarations, 5 contain sorry, 0 declared as axioms

Imports (2)
  1. theorem foo line 33 source

    no axioms what this means

    Proof uses: True.intro

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. theorem bar sorry line 39 source

    depends on sorry 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

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  3. theorem bar_symm sorry line 47 source

    depends on sorry 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

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  4. theorem bar_symm_explicit sorry line 55 source

    depends on sorry 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

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  5. theorem i_have_some_universes sorry line 63 source

    depends on sorry what this means

    Statement uses: Eq, Prod

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

    3 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  6. theorem this_works sorry line 73 source

    no axioms what this means

    Statement uses: True

    Proof uses: True.intro

    Tactic trace: 1 steps

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

  7. abbrev c line 82 source