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

doc(doc/changes): describe new "smart unfolding" feature

Browse source
This commit is contained in:
Leonardo de Moura 2018-01-09 16:47:32 -08:00
parent 60be2bf2aa
commit 5cd0f25c1e
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
doc/changes.md
View file

@ -78,6 +78,14 @@ master branch (aka work in progress branch)
This was problematic because we could only define abbreviations after the meta programming
framework was defined.
* Add "smart unfolding". The idea is to prevent internal compilation details
used by the equation compiler to "leak" during unification, tactic execution and
reduction. With "smart unfolding", the term `nat.add a (nat.succ b)` reduces
to `nat.succ (nat.add a b)` instead of `nat.succ (... incomprehensible mess ...)`.
This feature addresses a problem reported by many users.
See [issue #1794](https://github.com/leanprover/lean/issues/1794).
The command `set_option type_context.smart_unfolding false` disables this feature.
*Changes*
* Replace `inout` modifier in type class declarations with `out_param` modifier.