notation

forked-from-1kasper · Dec 30, 2023 · 2edeebc · 2edeebc
1 parent 198bef5
commit 2edeebc
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/GroundZero/Meta/Notation.lean b/GroundZero/Meta/Notation.lean
@@ -32,6 +32,8 @@ def revertDefaultProp : Delab := do {
   | stx     => return stx
 }
 
+macro "variables " vs:(ppSpace bracketedBinder)* : command => `(variable $vs*)
+
 syntax "Π " many1(ppSpace (binderIdent <|> bracketedBinder)) ", " term : term
 macro_rules | `(Π $xs*, $y) => `(∀ $xs*, $y)
 

diff --git a/GroundZero/Structures.lean b/GroundZero/Structures.lean
@@ -149,12 +149,12 @@ hott definition isNType : hlevel → Type u → Type u
 | −2            => contr
 | hlevel.succ n => λ A, Π (x y : A), isNType n (x = y)
 
-notation "is-" n "-type" => isNType n
+notation "is-" n:max "-type" => isNType n
 
 hott definition nType (n : hlevel) : Type (u + 1) :=
 Σ (A : Type u), is-n-type A
 
-notation n "-Type" => nType n
+notation n:max "-Type" => nType n
 macro n:term "-Type" l:level : term => `(nType.{$l} $n)
 
 hott lemma hlevel.cumulative {A : Type u} : Π (n : hlevel), is-n-type A → is-(hlevel.succ n)-type A