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

chore: fix doc

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-11 11:40:39 -08:00
parent d46cb80362
commit 03bd608b00
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
doc/thunk.md
View file

@ -52,13 +52,13 @@ def g (c : Bool) (x : Nat) : Nat :=
#eval g false 1000
```
In the following example, we use the macro `dbgTrace!` to demonstrate
In the following example, we use the macro `dbg_trace` to demonstrate
that the Lean runtime caches the value computed by a `Thunk`.
We remark that the macro `dbgTrace!` should be use for debugging purposes
We remark that the macro `dbg_trace` should be use for debugging purposes
only.
```lean
def add1 (x : Nat) : Nat :=
dbgTrace! "add1: {x}"
dbg_trace "add1: {x}"
x + 1
def double (x : Thunk Nat) : Nat :=
@ -78,7 +78,7 @@ Note that the message `add1: 2` is printed only once.
Now, consider the same example using `Unit -> Nat` instead of `Thunk Nat`.
```lean
def add1 (x : Nat) : Nat :=
dbgTrace! "add1: {x}"
dbg_trace "add1: {x}"
x + 1
def double (x : Unit -> Nat) : Nat :=
@ -97,7 +97,7 @@ def test (x : Nat) : Nat :=
```
Now, the message `add1: 2` is printed twice.
It may come as a surprise that it was printed twice instead of three times.
As we pointed out, `dbgTrace!` is a macro used for debugging purposes only,
As we pointed out, `dbg_trace` is a macro used for debugging purposes only,
and `add1` is still considered to be a pure function.
The Lean compiler performs common subexpression elimination when compiling `double`,
and the produced code for `double` executes `x ()` only once instead of twice.