From 0a2d05818e0a7bf0a06bb02410234c58a173c449 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 2 Mar 2023 19:56:16 +0100
Subject: [PATCH] fix fixities

---
 lib/Quox/Context.idr      |  2 --
 lib/Quox/Syntax/DimEq.idr |  2 +-
 lib/Quox/Syntax/Shift.idr | 11 +++--------
 lib/Quox/Syntax/Subst.idr |  2 --
 4 files changed, 4 insertions(+), 13 deletions(-)

diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index c566a4a..3713656 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -12,7 +12,6 @@ import Control.Monad.Identity
 %default total
 
 
-infixl 5 :<
 ||| a sequence of bindings under an existing context. each successive element
 ||| has one more bound variable, which correspond to all previous elements
 ||| as well as the surrounding context.
@@ -63,7 +62,6 @@ toList' : Telescope' a _ _ -> List a
 toList' = map snd . toList
 
 
-infixl 9 .
 public export
 (.) : Telescope tm from mid -> Telescope tm mid to -> Telescope tm from to
 tel1 . [<]         = tel1
diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index f1ca157..f13ae14 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -98,7 +98,7 @@ equal ZeroIsOne p q = True
 equal (C eqs)   p q = get eqs p == get eqs q
 
 
-infixl 5 :<?
+infixl 7 :<?
 export %inline
 (:<?) : DimEq d -> Maybe (Dim d) -> DimEq (S d)
 ZeroIsOne :<? d = ZeroIsOne
diff --git a/lib/Quox/Syntax/Shift.idr b/lib/Quox/Syntax/Shift.idr
index 6af6e7b..b03830e 100644
--- a/lib/Quox/Syntax/Shift.idr
+++ b/lib/Quox/Syntax/Shift.idr
@@ -144,7 +144,6 @@ shiftViaNatCorrect (SS by) i (LTESucc p) = cong VS $ shiftViaNatCorrect by i p
 %transform "Shift.shift" shift = shiftViaNat
 
 
-infixl 9 .
 public export
 (.) : Shift from mid -> Shift mid to -> Shift from to
 by . SZ    = by
@@ -154,14 +153,10 @@ private
 0 compNatProof : (by : Shift from mid) -> (bz : Shift mid to) ->
                  to = by.nat + bz.nat + from
 compNatProof by bz =
-  shiftDiff bz                       >>>
-  cong (bz.nat +) (shiftDiff by)     >>>
-  plusAssociative bz.nat by.nat from >>>
+  trans (shiftDiff bz) $
+  trans (cong (bz.nat +) (shiftDiff by)) $
+  trans (plusAssociative bz.nat by.nat from) $
   cong (+ from) (plusCommutative bz.nat by.nat)
- where
-  infixr 0 >>>
-  0 (>>>) : a = b -> b = c -> a = c
-  x >>> y = trans x y
 
 private %inline
 compViaNat' : (by : Shift from mid) -> (bz : Shift mid to) ->
diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr
index 9a0fa9c..39110a7 100644
--- a/lib/Quox/Syntax/Subst.idr
+++ b/lib/Quox/Syntax/Subst.idr
@@ -12,7 +12,6 @@ import Data.Vect
 %default total
 
 
-infixr 5 :::
 public export
 data Subst : (Nat -> Type) -> Nat -> Nat -> Type where
   Shift : Shift from to -> Subst env from to
@@ -60,7 +59,6 @@ shift : (by : Nat) -> Subst env from (by + from)
 shift by = Shift $ fromNat by
 
 
-infixl 9 .
 public export
 (.) : CanSubstSelf f => Subst f from mid -> Subst f mid to -> Subst f from to
 Shift by      . Shift bz   = Shift $ by . bz