From 45150c2a3bc511143014b5198aba7613cad302dc Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 3 Sep 2021 16:34:57 +0200
Subject: [PATCH] remove zeroes on types

---
 src/Quox/Name.idr         | 4 ++--
 src/Quox/Pretty.idr       | 6 +++---
 src/Quox/Syntax/Dim.idr   | 2 +-
 src/Quox/Syntax/Subst.idr | 2 +-
 src/Quox/Syntax/Term.idr  | 8 ++++----
 5 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/Quox/Name.idr b/src/Quox/Name.idr
index c432667..f8ed93f 100644
--- a/src/Quox/Name.idr
+++ b/src/Quox/Name.idr
@@ -9,7 +9,7 @@ public export
 data BaseName =
     UN String -- user-given name
 
-private 0 BRepr : Type
+private BRepr : Type
 BRepr = String
 
 private %inline brepr : BaseName -> BRepr
@@ -33,7 +33,7 @@ record Name where
   mods : SnocList String
   base : BaseName
 
-private 0 Repr : Type
+private Repr : Type
 Repr = (SnocList String, BRepr)
 
 private %inline repr : Name -> Repr
diff --git a/src/Quox/Pretty.idr b/src/Quox/Pretty.idr
index 8049a5b..a445c79 100644
--- a/src/Quox/Pretty.idr
+++ b/src/Quox/Pretty.idr
@@ -26,7 +26,7 @@ data HL
   | Free
   | Syntax
 
-private 0 HLRepr : Type
+private HLRepr : Type
 HLRepr = Nat
 
 private %inline hlRepr : HL -> Nat
@@ -54,7 +54,7 @@ data PPrec
   | SApp -- substitution application
   | Arg
 
-private 0 PrecRepr : Type
+private PrecRepr : Type
 PrecRepr = Nat
 
 private %inline precRepr : PPrec -> PrecRepr
@@ -109,7 +109,7 @@ record PrettyEnv where
   ||| surrounding precedence level
   prec    : PPrec
 
-public export %inline 0 HasEnv : (Type -> Type) -> Type
+public export %inline HasEnv : (Type -> Type) -> Type
 HasEnv = MonadReader PrettyEnv
 
 export
diff --git a/src/Quox/Syntax/Dim.idr b/src/Quox/Syntax/Dim.idr
index e445b2e..e58e98d 100644
--- a/src/Quox/Syntax/Dim.idr
+++ b/src/Quox/Syntax/Dim.idr
@@ -30,7 +30,7 @@ PrettyHL (Dim n) where
 
 
 public export
-0 DSubst : Nat -> Nat -> Type
+DSubst : Nat -> Nat -> Type
 DSubst = Subst Dim
 
 
diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index 4287a07..d34ac41 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -38,7 +38,7 @@ interface FromVar env => CanSubst env term where
   (//) : term from -> Subst env from to -> term to
 
 public export
-0 CanSubst1 : (Nat -> Type) -> Type
+CanSubst1 : (Nat -> Type) -> Type
 CanSubst1 f = CanSubst f f
 
 
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 49f6aef..6be5fcd 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -25,8 +25,8 @@ infixl 8 :#
 infixl 9 :@
 mutual
   public export
-  0 TSubst : Nat -> Nat -> Nat -> Type
-  TSubst d = Subst (Elim d)
+  TSubst : Nat -> Nat -> Nat -> Type
+  TSubst d = Subst (\n => Elim d n)
 
   ||| first argument `d` is dimension scope size, second `n` is term scope size
   public export
@@ -269,11 +269,11 @@ isCloT (E e)       = isCloE e
 isCloT _           = False
 
 ||| an elimination which is not a top level closure
-public export 0 NotCloElim : Nat -> Nat -> Type
+public export NotCloElim : Nat -> Nat -> Type
 NotCloElim d n = Subset (Elim d n) $ So . not . isCloE
 
 ||| a term which is not a top level closure
-public export 0 NotCloTerm : Nat -> Nat -> Type
+public export NotCloTerm : Nat -> Nat -> Type
 NotCloTerm d n = Subset (Term d n) $ So . not . isCloT