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

test: for simp [x] where x is a let-variable

Browse source
This commit is contained in:
Leonardo de Moura 2023-10-23 19:06:23 -07:00 • committed by Leonardo de Moura
parent a3642bd8d9
commit dbcc7966cf
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/run/letDeclSimp.lean Normal file
View file

@ -0,0 +1,12 @@
example (a : Nat) : let n := 0; n + a = a := by
intro n
fail_if_success simp (config := { zeta := false })
simp (config := { zeta := false }) [n]
example (a b : Nat) (h : a = b) : let n := 0; n + a = b := by
intro n
fail_if_success simp (config := { zeta := false })
trace_state
simp (config := { zeta := false }) [n]
trace_state
simp [h]