Closed abdoo8080 closed 1 year ago
It's awesome that we can finally reconstruct some proofs! On a first pass I noticed that the reconstruction seems to be adding theorems to the environment with unhygienic (user-accessible) names, which it probably shouldn't. For example in
#check th0 theorem disjunctive_syllogism (p q : Prop) : p ∨ q → ¬p → q := by smt #check th0
the first #check fails while the second one succeeds.
#check
It's awesome that we can finally reconstruct some proofs! On a first pass I noticed that the reconstruction seems to be adding theorems to the environment with unhygienic (user-accessible) names, which it probably shouldn't. For example in
the first
#checkfails while the second one succeeds.