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

chore: use cdot

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-06 16:32:20 -07:00
parent 911ed750ff
commit 39093188bf
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
doc/examples/interp.lean
View file

@ -131,7 +131,7 @@ We can make some simple test functions. Firstly, adding two inputs `fun x y => y
-/
def add : Expr ctx (Ty.fn Ty.int (Ty.fn Ty.int Ty.int)) :=
lam (lam (op (.+.) (var stop) (var (pop stop))))
lam (lam (op (·+·) (var stop) (var (pop stop))))
#eval add.interp Env.nil 10 20
@ -144,9 +144,9 @@ definition itself is non-terminating. We use two tricks to make sure Lean accept
-/
def fact : Expr ctx (Ty.fn Ty.int Ty.int) :=
lam (ife (op (.==.) (var stop) (val 0))
lam (ife (op (·==·) (var stop) (val 0))
(val 1)
(op (.*.) (delay fun _ => app fact (op (.-.) (var stop) (val 1))) (var stop)))
(op (·*·) (delay fun _ => app fact (op (·-·) (var stop) (val 1))) (var stop)))
decreasing_by sorry
#eval fact.interp Env.nil 10