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

chore(changes): universe max u v + 1

Browse source
This commit is contained in:
Leonardo de Moura 2017-07-07 12:59:21 -07:00
parent 8dcccd3bfc
commit ee612c8dd6
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/changes.md
View file

@ -88,6 +88,8 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
* Removed the redundant keywords `take` (replace with `assume`) and `suppose` (replace with the new anonymous `assume :`)
* Universes `max u v + 1` and `imax u v + 1` are now parsed as `(max u v) + 1` and `(imax u v) + 1`.
*API name changes*
* `list.dropn` => `list.drop`