From bc1aa21f09109807aa43f50946959a0dd034a6e6 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 3 Sep 2021 16:31:53 +0200
Subject: [PATCH 1/8] use dots for record fields

---
 src/Quox/Pretty.idr       | 9 ++++-----
 src/Quox/Syntax/Dim.idr   | 2 +-
 src/Quox/Syntax/Subst.idr | 2 +-
 src/Quox/Syntax/Term.idr  | 2 +-
 4 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/Quox/Pretty.idr b/src/Quox/Pretty.idr
index e44d334..8049a5b 100644
--- a/src/Quox/Pretty.idr
+++ b/src/Quox/Pretty.idr
@@ -114,11 +114,11 @@ HasEnv = MonadReader PrettyEnv
 
 export
 ifUnicode : HasEnv m => (uni, asc : Lazy a) -> m a
-ifUnicode uni asc = if unicode !ask then [|uni|] else [|asc|]
+ifUnicode uni asc = if (!ask).unicode then [|uni|] else [|asc|]
 
 export
 parensIfM : HasEnv m => PPrec -> Doc HL -> m (Doc HL)
-parensIfM d doc = pure $ parensIf (prec !ask > d) doc
+parensIfM d doc = pure $ parensIf ((!ask).prec > d) doc
 
 export
 withPrec : HasEnv m => PPrec -> m a -> m a
@@ -164,9 +164,8 @@ export PrettyHL Name     where prettyM = pure . pretty . toDots
 export
 prettyStr : PrettyHL a => {default True unicode : Bool} -> a -> String
 prettyStr {unicode} =
-  renderString .
-  layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) .
-  pretty0 {unicode}
+  let layout = layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) in
+  renderString . layout . pretty0 {unicode}
 
 
 export
diff --git a/src/Quox/Syntax/Dim.idr b/src/Quox/Syntax/Dim.idr
index cba8b2e..e445b2e 100644
--- a/src/Quox/Syntax/Dim.idr
+++ b/src/Quox/Syntax/Dim.idr
@@ -37,7 +37,7 @@ DSubst = Subst Dim
 export %inline
 prettyDSubst : Pretty.HasEnv m => DSubst from to -> m (Doc HL)
 prettyDSubst th =
-  prettySubstM prettyM (dnames !ask) DVar
+  prettySubstM prettyM (!ask).dnames DVar
     !(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
 
 
diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index 497d6cc..4287a07 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -118,4 +118,4 @@ prettySubstM pr names bnd op cl th =
 ||| prints with [square brackets] and the `TVar` highlight for variables
 export
 PrettyHL (f to) => PrettyHL (Subst f from to) where
-  prettyM th = prettySubstM prettyM (tnames !ask) TVar "[" "]" th
+  prettyM th = prettySubstM prettyM (!ask).tnames TVar "[" "]" th
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 8a6ab99..9247619 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -167,7 +167,7 @@ mutual
 
   export covering
   prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
-  prettyTSubst s = prettySubstM prettyM (tnames !ask) TVar "[" "]" s
+  prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
 
   export covering
   prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)

From e03b4a4286cd67c7b39330e1780879e7ad679637 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 3 Sep 2021 16:32:22 +0200
Subject: [PATCH 2/8] give some subterms better names

---
 src/Quox/Syntax/Term.idr | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 9247619..49f6aef 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -36,17 +36,17 @@ mutual
 
     ||| function type
     Pi  : (qty, qtm : Qty) -> (x : Name) ->
-          (a : Term d n) -> (b : Term d (S n)) -> Term d n
+          (arg : Term d n) -> (res : Term d (S n)) -> Term d n
     ||| function term
-    Lam : (x : Name) -> (t : Term d (S n)) -> Term d n
+    Lam : (x : Name) -> (body : Term d (S n)) -> Term d n
 
     ||| elimination
     E : (e : Elim d n) -> Term d n
 
     ||| term closure/suspended substitution
-    CloT  : (s : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
+    CloT  : (tm : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
     ||| dimension closure/suspended substitution
-    DCloT : (s : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
+    DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
 
   ||| first argument `d` is dimension scope size, second `n` is term scope size
   public export
@@ -57,15 +57,15 @@ mutual
     B : (i : Var n) -> Elim d n
 
     ||| term application
-    (:@) : (f : Elim d n) -> (s : Term d n) -> Elim d n
+    (:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
 
     ||| type-annotated term
-    (:#) : (s, a : Term d n) -> Elim d n
+    (:#) : (tm, ty : Term d n) -> Elim d n
 
     ||| term closure/suspended substitution
-    CloE  : (e : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
+    CloE  : (el : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
     ||| dimension closure/suspended substitution
-    DCloE : (e : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
+    DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
 
 %name Term s, t, r
 %name Elim e, f
@@ -323,8 +323,8 @@ parameters {auto _ : Alternative f}
   ||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)`
   export
   betaLam1 : Elim d n -> f (Elim d n)
-  betaLam1 ((Lam {t, _} :# Pi {a, b, _}) :@ s) =
-    pure $ (t :# b) // (s :# a ::: id)
+  betaLam1 ((Lam {body, _} :# Pi {arg, res, _}) :@ s) =
+    pure $ (body :# res) // (s :# arg ::: id)
   betaLam1 _ = empty
 
   ||| `(e ⦂ A) >>> e`    [if `e` is an elim]

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 3/8] 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
 
 

From 06e5c098960b6c83711804d539fd7df36bba9f01 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 3 Sep 2021 16:38:26 +0200
Subject: [PATCH 4/8] remove old file i forgot about

---
 src/Quox/Ctx.idr         | 98 ----------------------------------------
 src/Quox/Syntax/Term.idr |  1 -
 2 files changed, 99 deletions(-)
 delete mode 100644 src/Quox/Ctx.idr

diff --git a/src/Quox/Ctx.idr b/src/Quox/Ctx.idr
deleted file mode 100644
index 56a2991..0000000
--- a/src/Quox/Ctx.idr
+++ /dev/null
@@ -1,98 +0,0 @@
-module Quox.Ctx
-
-import Data.Nat
-import Data.Fin
-import Data.SnocList
-import Data.DPair
-
-
-%default total
-
-public export
-data Ctx : Nat -> (Nat -> Type) -> Type where
-  Lin  : Ctx 0 f
-  (:<) : Ctx n f -> f n -> Ctx (S n) f
-
-%name Ctx ctx
-
-
-public export
-0 Ctx' : Nat -> Type -> Type
-Ctx' n a = Ctx n (\_ => a)
-
-
-public export
-toSList : Ctx n f -> SnocList (Exists f)
-toSList [<]        = [<]
-toSList (ctx :< x) = toSList ctx :< Evidence _ x
-
-public export
-toSList' : Ctx' n a -> SnocList a
-toSList' ctx = map (.snd) $ toSList ctx
-
-public export
-fromSList' : (xs : SnocList a) -> Ctx' (length xs) a
-fromSList' [<]       = [<]
-fromSList' (sx :< x) = fromSList' sx :< x
-
-
-public export
-0 Weaken : (Nat -> Type) -> Type
-Weaken f = forall n. (by : Nat) -> (1 x : f n) -> f (by + n)
-
-public export
-interface Weak f where weakN : Weaken f
-
-public export
-weak : Weak f => (1 x : f n) -> f (S n)
-weak = weakN 1
-
-
-public export
-lookBy : Weaken f -> Ctx n f -> (1 _ : Fin n) -> f n
-lookBy w = go 0 where
-  go : forall n. (by : Nat) -> Ctx n f -> (1 _ : Fin n) -> f (by + n)
-  go by (ctx :< x) (FZ {k})   =
-    rewrite sym $ plusSuccRightSucc by k in w (S by) x
-  go by (ctx :< x) (FS {k} i) =
-    rewrite sym $ plusSuccRightSucc by k in go (S by) ctx i
-
-public export
-look : Weak f => Ctx n f -> (1 _ : Fin n) -> f n
-look = lookBy weakN
-
-infixl 9 !!
-public export
-(!!) : Ctx' n a -> (1 _ : Fin n) -> a
-(!!) = lookBy (\_, x => x)
-
-
-public export
-map : (forall n. f n -> g n) -> (1 _ : Ctx n f) -> Ctx n g
-map f [<]        = [<]
-map f (ctx :< x) = map f ctx :< f x
-
-
-public export
-(forall n. Eq (f n)) => Eq (Ctx n f) where
-  [<]         == [<]         = True
-  (ctx1 :< x) == (ctx2 :< y) = ctx1 == ctx2 && x == y
-
-public export
-(forall n. Ord (f n)) => Ord (Ctx n f) where
-  compare [<]         [<]         = EQ
-  compare (ctx1 :< x) (ctx2 :< y) = compare ctx1 ctx2 <+> compare x y
-
-
-||| like `Exists` but only shows the second part
-private
-data ShowWrapper : (Nat -> Type) -> Type where
-  SW : f n -> ShowWrapper f
-
-private
-(forall n. Show (f n)) => Show (ShowWrapper f) where
-  showPrec d (SW x) = showPrec d x
-
-export
-(forall n. Show (f n)) => Show (Ctx n f) where
-  show = show . map (\x => SW {f} x.snd) . toSList
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 6be5fcd..91efaf9 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -1,6 +1,5 @@
 module Quox.Syntax.Term
 
-import public Quox.Ctx
 import public Quox.Syntax.Var
 import public Quox.Syntax.Shift
 import public Quox.Syntax.Subst

From d41ab0897cabc8999e59b5f0a39d72b7d99a7b89 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 3 Sep 2021 17:10:20 +0200
Subject: [PATCH 5/8] remove some public exports that probably aren't needed

---
 src/Quox/Pretty.idr       | 4 ++--
 src/Quox/Syntax/Shift.idr | 2 +-
 src/Quox/Syntax/Term.idr  | 4 ++--
 src/Quox/Syntax/Var.idr   | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Quox/Pretty.idr b/src/Quox/Pretty.idr
index a445c79..a9296ba 100644
--- a/src/Quox/Pretty.idr
+++ b/src/Quox/Pretty.idr
@@ -137,11 +137,11 @@ public export
 interface PrettyHL a where
   prettyM : HasEnv m => a -> m (Doc HL)
 
-public export %inline
+export %inline
 pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL)
 pretty0M = local {prec := Outer} . prettyM
 
-public export %inline
+export %inline
 pretty0 : PrettyHL a => {default True unicode : Bool} -> a -> Doc HL
 pretty0 x {unicode} =
   let env = MakePrettyEnv {dnames = [], tnames = [], unicode, prec = Outer} in
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
index dfee608..471f13f 100644
--- a/src/Quox/Syntax/Shift.idr
+++ b/src/Quox/Syntax/Shift.idr
@@ -49,7 +49,7 @@ toEqv Refl {by = SZ}      = EqSZ
 toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl {by}
 
 
-public export
+export
 0 shiftDiff : (by : Shift from to) -> to = by.nat + from
 shiftDiff SZ      = Refl
 shiftDiff (SS by) = cong S $ shiftDiff by
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 91efaf9..d892157 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -332,10 +332,10 @@ parameters {auto _ : Alternative f}
   upsilon1 (E e :# _) = pure e
   upsilon1 _          = empty
 
-  public export
+  export
   step : Elim d n -> f (Elim d n)
   step e = betaLam1 e <|> upsilon1 e
 
-public export
+export
 step' : Elim d n -> Elim d n
 step' e = fromMaybe e $ step e
diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index 513a057..976b3d7 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -68,7 +68,7 @@ public export %inline
 V : (i : Nat) -> {auto 0 p : i `LT` n} -> Var n
 V i {p} = fromNatWith i p
 
-public export %inline
+export %inline
 tryFromNat : Alternative f => (n : Nat) -> Nat -> f (Var n)
 tryFromNat n i =
   case i `isLT` n of

From 6c05a348d5e697ee77ee91bf4aa1bf36e522fe78 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 3 Sep 2021 17:10:50 +0200
Subject: [PATCH 6/8] formatting fixes & tweaks

---
 src/Quox/Syntax/Subst.idr | 2 +-
 src/Quox/Syntax/Term.idr  | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index d34ac41..34b5b34 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -52,7 +52,7 @@ public export
 
 public export
 CanSubst Var Var where
-  i    // Shift by     = shift by i
+  i    // Shift by   = shift by i
   VZ   // (t ::: th) = t
   VS i // (t ::: th) = i // th
 
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index d892157..ff7f2a6 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -295,7 +295,7 @@ mutual
   pushSubstsT' th ph (Lam x t) =
     Element (Lam x $ subs t th $ push ph) Oh
   pushSubstsT' th ph (E e) =
-    case pushSubstsE' th ph e of Element e' prf => Element (E e') prf
+    let Element e prf = pushSubstsE' th ph e in Element (E e) prf
   pushSubstsT' th ph (CloT  s ps) =
     pushSubstsT' th (comp' th ps ph) s
   pushSubstsT' th ph (DCloT s ps) =
@@ -319,7 +319,7 @@ mutual
 
 
 parameters {auto _ : Alternative f}
-  ||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)`
+  ||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)]`
   export
   betaLam1 : Elim d n -> f (Elim d n)
   betaLam1 ((Lam {body, _} :# Pi {arg, res, _}) :@ s) =

From 6da33625f8e7858bf383751ee62b76c9449f71bd Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 3 Sep 2021 17:54:52 +0200
Subject: [PATCH 7/8] remove an (.int). no one likes ints

---
 src/Quox/Syntax/Term.idr | 4 ++++
 src/Quox/Syntax/Var.idr  | 8 --------
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index ff7f2a6..3c0c576 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -277,10 +277,14 @@ NotCloTerm d n = Subset (Term d n) $ So . not . isCloT
 
 
 mutual
+  ||| if the input term has any top-level closures, push them under one layer of
+  ||| syntax
   export
   pushSubstsT : Term d n -> NotCloTerm d n
   pushSubstsT s = pushSubstsT' id id s
 
+  ||| if the input elimination has any top-level closures, push them under one
+  ||| layer of syntax
   export
   pushSubstsE : Elim d n -> NotCloElim d n
   pushSubstsE e = pushSubstsE' id id e
diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index 976b3d7..ca5747b 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -99,14 +99,6 @@ toFromNat 0     (LTESucc x) = Refl
 toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
 
 
-public export
-(.int) : Var n -> Integer
-i.int = natToInteger i.nat
-%builtin NaturalToInteger Var.(.int)
-
-public export Cast (Var n) Integer where cast i = i.int
-
-
 -- not using %transform like other things because weakSpec requires the proof
 -- to be relevant. but since only `LTESucc` is ever possible that seems
 -- to be a bug?

From 5baade8dd593277ebf3f149ae9ce528aa9b14491 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 3 Sep 2021 17:56:04 +0200
Subject: [PATCH 8/8] Many => Any

---
 src/Quox/Syntax/Qty.idr | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr
index 4689d2d..90c0783 100644
--- a/src/Quox/Syntax/Qty.idr
+++ b/src/Quox/Syntax/Qty.idr
@@ -6,14 +6,14 @@ import Data.Fin
 
 
 public export
-data Qty = Zero | One | Many
+data Qty = Zero | One | Any
 %name Qty.Qty pi, rh
 
 private Repr : Type
 Repr = Fin 3
 
 private %inline repr : Qty -> Repr
-repr pi = case pi of Zero => 0; One => 1; Many => 2
+repr pi = case pi of Zero => 0; One => 1; Any => 2
 
 export Eq  Qty where (==) = (==) `on` repr
 export Ord Qty where compare = compare `on` repr
@@ -25,7 +25,7 @@ PrettyHL Qty where
     case pi of
       Zero => ifUnicode "𝟬" "0"
       One  => ifUnicode "𝟭" "1"
-      Many => ifUnicode "𝛚" "*"
+      Any  => ifUnicode "𝛚" "*"
 
 export %inline
 prettyQtyBinds : Pretty.HasEnv m => List Qty -> m (Doc HL)
@@ -38,7 +38,7 @@ public export
 (+) : Qty -> Qty -> Qty
 Zero + rh   = rh
 pi   + Zero = pi
-_    + _    = Many
+_    + _    = Any
 
 public export
 (*) : Qty -> Qty -> Qty
@@ -46,9 +46,9 @@ Zero * _    = Zero
 _    * Zero = Zero
 One  * rh   = rh
 pi   * One  = pi
-Many * Many = Many
+Any  * Any  = Any
 
 infix 6 <=.
 public export
 (<=.) : Qty -> Qty -> Bool
-pi <=. rh = rh == Many || pi == rh
+pi <=. rh = rh == Any || pi == rh