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] 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) =