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

chore: typo

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-29 13:40:49 -08:00
parent dfd1f23030
commit 7a622b2a85
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/thunks.md
View file

@ -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,
and `add1` is still considered to be pure function.
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.
This transformation is safe because `x : Unit -> Nat` is pure.