This commit is contained in:
rhiannon morris 2022-11-01 21:07:52 +01:00
parent e7272333cb
commit 23c008b57a

View file

@ -110,7 +110,7 @@ export
ssDownEqv SZ = EqSS EqSZ
ssDownEqv (SS by) = EqSS $ ssDownEqv by
private
private %inline
ssDownViaNat : Shift (S from) to -> Shift from to
ssDownViaNat by =
rewrite shiftDiff by in
@ -125,12 +125,12 @@ shift : Shift from to -> Var from -> Var to
shift SZ i = i
shift (SS by) i = VS $ shift by i
private
private %inline
shiftViaNat' : (by : Shift from to) -> (i : Var from) ->
(0 p : by.nat + i.nat `LT` to) -> Var to
shiftViaNat' by i p = V $ by.nat + i.nat
private
private %inline
shiftViaNat : Shift from to -> Var from -> Var to
shiftViaNat by i = shiftViaNat' by i $ shiftVarLT by i
@ -163,12 +163,12 @@ compNatProof by bz =
0 (>>>) : a = b -> b = c -> a = c
x >>> y = trans x y
private
private %inline
compViaNat' : (by : Shift from mid) -> (bz : Shift mid to) ->
Shift from (by.nat + bz.nat + from)
compViaNat' by bz = fromNat $ by.nat + bz.nat
private
private %inline
compViaNat : (by : Shift from mid) -> (bz : Shift mid to) -> Shift from to
compViaNat by bz = rewrite compNatProof by bz in compViaNat' by bz
@ -207,12 +207,13 @@ public export
interface CanShift f where
(//) : f from -> Shift from to -> f to
export CanShift Var where i // by = shift by i
export %inline
CanShift Var where i // by = shift by i
namespace CanShift
public export
public export %inline
[Map] (Functor f, CanShift tm) => CanShift (f . tm) where
x // by = map (// by) x
public export
public export %inline
[Const] CanShift (\_ => a) where x // _ = x