test: add let_fun pretty printing test

This commit is contained in:
Leonardo de Moura 2021-09-16 10:14:42 -07:00
parent 4c0ae51a81
commit 1c00f29043
2 changed files with 20 additions and 0 deletions

10
tests/lean/letFun.lean Normal file
View file

@ -0,0 +1,10 @@
#check
let_fun f x := x * 2
let_fun x := 1
let_fun y := x + 1
f (y + x)
example (a b : Nat) (h1 : a = 0) (h2 : b = 0) : (let_fun x := a + 1; x + x) > b := by
simp (config := { beta := false }) [h1]
traceState
simp [h2]

View file

@ -0,0 +1,10 @@
let_fun f := fun x => x * 2;
let_fun x := 1;
let_fun y := x + 1;
f (y + x) : Nat
a b : Nat
h1 : a = 0
h2 : b = 0
⊢ (let_fun x := 1;
x + x) >
b