Skip to content

Commit

Permalink
Fix tests
Browse files Browse the repository at this point in the history
  • Loading branch information
JLimperg committed Nov 13, 2023
1 parent d754489 commit bf5ab42
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 4 deletions.
6 changes: 6 additions & 0 deletions tests/EraseSimp.lean.expected
Original file line number Diff line number Diff line change
@@ -1 +1,7 @@
tests/EraseSimp.lean:20:2: error: tactic 'aesop' failed, made no progress
m n : Nat
⊢ n + m = m + n
tests/EraseSimp.lean:24:2: error: tactic 'aesop' failed, made no progress
m n : Nat
⊢ n + m = m + n
tests/EraseSimp.lean:28:2: error: aesop: 'Nat.add_comm' is not registered (with the given features) in any rule set.
9 changes: 8 additions & 1 deletion tests/TraceProof.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,13 @@ import Aesop

set_option aesop.check.all true

set_option trace.aesop.proof true in
set_option trace.aesop.proof true

example : α := by
aesop

@[aesop norm simp]
def F := False

example : F := by
aesop
8 changes: 5 additions & 3 deletions tests/TraceProof.lean.expected
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
tests/TraceProof.lean:13:2: warning: aesop: failed to prove the goal after exhaustive search.
tests/TraceProof.lean:12:15: error: unsolved goals
tests/TraceProof.lean:14:2: error: tactic 'aesop' failed, made no progress
α : Sort ?u.5
⊢ α
[aesop.proof] <no proof>
tests/TraceProof.lean:20:2: warning: aesop: failed to prove the goal after exhaustive search.
tests/TraceProof.lean:19:15: error: unsolved goals
⊢ False
[aesop.proof] id ?m.38

0 comments on commit bf5ab42

Please sign in to comment.