reorder clauses in Subst.(.)

This commit is contained in:
rhiannon morris 2021-09-25 20:13:51 +02:00
parent cdcd926347
commit eae97a7b9d

View file

@ -65,8 +65,8 @@ shift by = Shift $ fromNat by
infixl 9 . infixl 9 .
public export public export
(.) : CanSubst1 f => Subst f from mid -> Subst f mid to -> Subst f from to (.) : CanSubst1 f => Subst f from mid -> Subst f mid to -> Subst f from to
Shift by . Shift bz = Shift $ by . bz
Shift SZ . ph = ph Shift SZ . ph = ph
Shift (SS by) . Shift bz = Shift $ SS by . bz
Shift (SS by) . (t ::: th) = Shift by . th Shift (SS by) . (t ::: th) = Shift by . th
(t ::: th) . ph = (t // ph) ::: (th . ph) (t ::: th) . ph = (t // ph) ::: (th . ph)