Commit e475fff1 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix level for let notation.

parent e5fcec8f
......@@ -47,7 +47,7 @@ Module notations.
Notation "λ: x , e" := (Lam x e%L)
(at level 102, x at level 1, e at level 200) : lang_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L)
(at level 102, x at level 1, e1 at level 1, e2 at level 200) : lang_scope.
(at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
Notation "e1 ; e2" := (Lam "" e2%L e1%L)
(at level 100, e2 at level 200) : lang_scope.
End notations.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment