From 65e45dcc7921b8c76f067004b195fbc65b817dbe Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 26 Sep 2021 10:55:07 +0200
Subject: [PATCH 1/4] use stdlib Elem and add note why not also stdlib
 OpenUnion

---
 src/Quox/Error.idr | 18 ++++--------------
 1 file changed, 4 insertions(+), 14 deletions(-)

diff --git a/src/Quox/Error.idr b/src/Quox/Error.idr
index a78cabb..bbe8b0f 100644
--- a/src/Quox/Error.idr
+++ b/src/Quox/Error.idr
@@ -1,5 +1,7 @@
 module Quox.Error
 
+import Data.List.Elem
+
 import Control.Monad.Identity
 import Control.Monad.Trans
 import Control.Monad.Reader
@@ -10,20 +12,6 @@ import Control.Monad.RWS
 %default total
 
 
-||| a proof that an element is in a list. unlike the standard library one, this
-||| is represented as a single number at runtime.
-public export
-data Elem : a -> List a -> Type where
-  Here  : x `Elem` (x :: xs)
-  There : x `Elem` xs -> x `Elem` (y :: xs)
-%builtin Natural Elem
-
-export
-Uninhabited (x `Elem` []) where
-  uninhabited Here      impossible
-  uninhabited (There _) impossible
-
-
 ||| a representation of a list's length. this is used in the `Ord` instance to
 ||| transform the `Ord` constraints into `Eq`s
 public export
@@ -40,6 +28,8 @@ record OneOf types where
   constructor One
   elem    : type `Elem` types
   1 value : type
+-- this is basically the same as Data.OpenUnion, but using Elem instead of
+-- AtIndex is much easier for some stuff here e.g. `get`
 
 export
 Uninhabited (OneOf []) where uninhabited x = uninhabited x.elem

From 81fc802fa869fa206bfe1bec131639ba3c36b5a8 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 26 Sep 2021 11:11:30 +0200
Subject: [PATCH 2/4] move SomeTerm stuff

---
 src/Quox/Eval.idr        | 24 ------------------------
 src/Quox/Syntax/Term.idr | 24 ++++++++++++++++++++++++
 2 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/src/Quox/Eval.idr b/src/Quox/Eval.idr
index e026814..0e3e878 100644
--- a/src/Quox/Eval.idr
+++ b/src/Quox/Eval.idr
@@ -15,30 +15,6 @@ import Data.SortedMap
 %default total
 
 
-public export Exists2 : (ty1 -> ty2 -> Type) -> Type
-Exists2 t = Exists (\a => Exists (\b => t a b))
-
-parameters {0 t : ty -> Type}
-  private %inline some : t a -> Exists t
-  some t = Evidence _ t
-
-parameters {0 t : ty1 -> ty2 -> Type}
-  private %inline some2 : t a b -> Exists2 t
-  some2 t = some $ some t
-
-||| A term of some unknown scope sizes.
-public export SomeTerm : Type
-SomeTerm = Exists2 Term
-
-||| An elimination of some unknown scope sizes.
-public export SomeElim : Type
-SomeElim = Exists2 Elim
-
-||| A dimension of some unknown scope size.
-public export SomeDim : Type
-SomeDim = Exists Dim
-
-
 public export
 record Global where
   constructor G
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index d10d41d..b1441c5 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -368,3 +368,27 @@ parameters {auto _ : Alternative f}
 export
 step' : Elim d n -> Elim d n
 step' e = fromMaybe e $ step e
+
+
+public export Exists2 : (ty1 -> ty2 -> Type) -> Type
+Exists2 t = Exists (\a => Exists (\b => t a b))
+
+parameters {0 t : ty -> Type}
+  public export %inline some : t a -> Exists t
+  some t = Evidence _ t
+
+parameters {0 t : ty1 -> ty2 -> Type}
+  public export %inline some2 : t a b -> Exists2 t
+  some2 t = some $ some t
+
+||| A term of some unknown scope sizes.
+public export SomeTerm : Type
+SomeTerm = Exists2 Term
+
+||| An elimination of some unknown scope sizes.
+public export SomeElim : Type
+SomeElim = Exists2 Elim
+
+||| A dimension of some unknown scope size.
+public export SomeDim : Type
+SomeDim = Exists Dim

From 37230a803257fff09f107e05a47b0cd63a037041 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 21 Nov 2021 14:59:27 +0100
Subject: [PATCH 3/4] tweak some type signatures

---
 src/Quox/Context.idr | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index 65e5328..dc66a8b 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -169,14 +169,14 @@ zipWith3Lazy : forall tm1, tm2, tm3, tm4.
                Telescope tm2 from to ->
                Telescope tm3 from to ->
                Telescope (\n => Lazy (tm4 n)) from to
-zipWith3Lazy f = zipWith3 (\x, y, z => delay $ f x y z)
+zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
 
 
 export
-lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
+lengthPrf : Telescope _ from to -> Subset Nat $ \len => len + from = to
 lengthPrf [<]        = Element 0 Refl
-lengthPrf (tel :< _) =
-  let len = lengthPrf tel in Element (S len.fst) (cong S len.snd)
+lengthPrf (tel :< _) = let len = lengthPrf tel in
+                       Element (S len.fst) (cong S len.snd)
 
 public export %inline
 length : Telescope {} -> Nat
@@ -196,40 +196,40 @@ parameters {auto _ : Monoid a}
   foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
 
   export %inline
-  fold : Telescope (\x => a) from to -> a
+  fold : Telescope' a from to -> a
   fold = foldMap id
 
   ||| like `fold` but calculate the elements only when actually appending
   export %inline
-  foldLazy : Telescope (\x => Lazy a) from to -> a
+  foldLazy : Telescope' (Lazy a) from to -> a
   foldLazy = foldMap force
 
 
 export %inline
-and : Telescope' (Lazy Bool) from to -> Bool
+and : Telescope' (Lazy Bool) _ _ -> Bool
 and = force . fold @{All}
 
 export %inline
-all : (forall n. f n -> Bool) -> Telescope f from to -> Bool
+all : (forall n. tm n -> Bool) -> Telescope tm _ _ -> Bool
 all p = and . map (delay . p)
 
 export %inline
-all2 : (forall n. f n -> g n -> Bool) ->
-       Telescope f from to -> Telescope g from to -> Bool
+all2 : (forall n. tm n -> tm2 n -> Bool) ->
+       Telescope tm from to -> Telescope tm2 from to -> Bool
 all2 p = and .: zipWithLazy p
 
 
 export %inline
-or : Telescope' (Lazy Bool) from to -> Bool
+or : Telescope' (Lazy Bool) _ _ -> Bool
 or = force . fold @{Any}
 
 export %inline
-any : (forall n. f n -> Bool) -> Telescope f from to -> Bool
+any : (forall n. tm n -> Bool) -> Telescope tm _ _ -> Bool
 any p = or . map (delay . p)
 
 export %inline
-any2 : (forall n. f n -> g n -> Bool) ->
-       Telescope f from to -> Telescope g from to -> Bool
+any2 : (forall n. tm1 n -> tm2 n -> Bool) ->
+       Telescope tm1 from to -> Telescope tm2 from to -> Bool
 any2 p = or .: zipWithLazy p
 
 

From fce293caa7f0779ae3297b20d9f74395eaabfcc1 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 21 Nov 2021 14:59:41 +0100
Subject: [PATCH 4/4] fix an outdated comment

---
 src/Quox/Syntax/Subst.idr | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index 2658e0a..6035633 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -90,16 +90,14 @@ drop1 (Shift by) = Shift $ drop1 by
 drop1 (t ::: th) = th
 
 
-||| `prettySubst pr bnd op cl unicode th` pretty-prints the substitution `th`,
+||| `prettySubst pr names bnd op cl th` pretty-prints the substitution `th`,
 ||| with the following arguments:
 |||
 ||| * `th : Subst f from to`
-||| * `pr : (unicode : Bool) -> f to -> m (Doc HL)` prints a single element
+||| * `pr : f to -> m (Doc HL)` prints a single element
 ||| * `names : List Name` is a list of known bound var names
 ||| * `bnd : HL` is the highlight to use for bound variables being subsituted
 ||| * `op, cl : Doc HL` are the opening and closing brackets
-||| * `unicode : Bool` is whether to use unicode characters in the output
-|||   (also passed into `pr`)
 export
 prettySubstM : Pretty.HasEnv m =>
                (pr : f to -> m (Doc HL)) ->