From ee612c8dd621496c53928db0630df7be984db5af Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Jul 2017 12:59:21 -0700 Subject: [PATCH] chore(changes): universe `max u v + 1` --- doc/changes.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/changes.md b/doc/changes.md index c3a41e9a27..866a4f3936 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -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`