max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2024-01-22 20:15:48 -08:00 • committed by Scott Morrison
parent 8db28ac32f
commit 266075b8a4
3 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/simproc1.lean
View file

@ -5,9 +5,9 @@ def foo (x : Nat) : Nat :=
open Lean Meta
simproc reduceFoo (foo _) := fun e => OptionT.run do
guard (e.isAppOfArity ``foo 1)
let n ← Nat.fromExpr? e.appArg!
simproc reduceFoo (foo _) := fun e => do
unless e.isAppOfArity ``foo 1 do return .continue
let some n ← Nat.fromExpr? e.appArg! | return .continue
return .done { expr := mkNatLit (n+10) }
example : x + foo 2 = 12 + x := by

2
tests/lean/simp_trace.lean.expected.out
View file

@ -49,7 +49,7 @@ Try this: simp only [h, Nat.sub_add_cancel]
Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel]
[Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True
[Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
[Meta.Tactic.simp.rewrite] @eq_self:1000, (if h : 1 ≤ x then x else 0) = if _h : 1 ≤ x then x else 0 ==> True
[Meta.Tactic.simp.rewrite] @eq_self:1000, (if h : 1 ≤ x then x else 0) = if h : 1 ≤ x then x else 0 ==> True
Try this: simp only [and_self]
[Meta.Tactic.simp.rewrite] and_self:1000, b ∧ b ==> b
[Meta.Tactic.simp.rewrite] iff_self:1000, a ∧ b ↔ a ∧ b ==> True

4
tests/lean/simprocTrace.lean
View file

@ -5,8 +5,8 @@ def foo (x : Nat) : Nat :=
x + 10
simproc reduce_foo (foo _) := fun e => open Lean Meta in do
let some n ← evalNat e.appArg! |>.run | return none
return some (.done { expr := mkNatLit (n+10) })
let some n ← evalNat e.appArg! |>.run | return .continue
return .done { expr := mkNatLit (n+10) }
set_option tactic.simp.trace true
example : x + foo 2 = 12 + x := by