rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

oops Shift.drop1 and ssDown were the same

Browse source
This commit is contained in:
rhiannon morris 2022-06-24 11:28:25 +02:00
parent 956c677614
commit 77e94a3033
4 changed files with 4 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
lib/Quox/Context.idr
View file

@ -73,8 +73,8 @@ tel1 . (tel2 :< s) = (tel1 . tel2) :< s
public export public export
getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) -> getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) ->
Shift len out -> Context tm len -> Var len -> tm out Shift len out -> Context tm len -> Var len -> tm out
getShiftWith shft by (ctx :< t) VZ = t `shft` drop1 by getShiftWith shft by (ctx :< t) VZ = t `shft` ssDown by
getShiftWith shft by (ctx :< t) (VS i) = getShiftWith shft (drop1 by) ctx i getShiftWith shft by (ctx :< t) (VS i) = getShiftWith shft (ssDown by) ctx i
public export %inline public export %inline
getShift : CanShift tm => Shift len out -> Context tm len -> Var len -> tm out getShift : CanShift tm => Shift len out -> Context tm len -> Var len -> tm out

2
lib/Quox/Syntax/DimEq.idr
View file

@ -149,7 +149,7 @@ private
0 newGetShift : (d : Nat) -> (i : Var d) -> (by : Shift d d') -> 0 newGetShift : (d : Nat) -> (i : Var d) -> (by : Shift d d') ->
getShift' by (new' {d}) i = Nothing getShift' by (new' {d}) i = Nothing
newGetShift (S d) VZ by = Refl newGetShift (S d) VZ by = Refl
newGetShift (S d) (VS i) by = newGetShift d i (drop1 by) newGetShift (S d) (VS i) by = newGetShift d i (ssDown by)
export export
0 newGet' : (d : Nat) -> (i : Var d) -> get' (new' {d}) i = Nothing 0 newGet' : (d : Nat) -> (i : Var d) -> get' (new' {d}) i = Nothing

24
lib/Quox/Syntax/Shift.idr
View file

@ -195,30 +195,6 @@ prettyShift bnd by =
export PrettyHL (Shift from to) where prettyM = prettyShift TVar export PrettyHL (Shift from to) where prettyM = prettyShift TVar
||| Drops the innermost variable from the input scope.
public export
drop1 : Shift (S from) to -> Shift from to
drop1 SZ = SS SZ
drop1 (SS by) = SS (drop1 by)
private
drop1ViaNat : Shift (S from) to -> Shift from to
drop1ViaNat by =
rewrite shiftDiff by in
rewrite sym $ plusSuccRightSucc by.nat from in
fromNat (S by.nat)
private
0 drop1ViaNatCorrect : (by : Shift (S from) to) -> drop1ViaNat by = drop1 by
drop1ViaNatCorrect SZ = Refl
drop1ViaNatCorrect (SS by) =
rewrite plusSuccRightSucc by.nat from in
rewrite sym $ shiftDiff by in
cong SS $ drop1ViaNatCorrect by
%transform "Shift.drop1" drop1 by = drop1ViaNat by
infixl 8 // infixl 8 //
public export public export
interface CanShift f where interface CanShift f where

2
lib/Quox/Syntax/Subst.idr
View file

@ -86,7 +86,7 @@ push th = fromVar VZ ::: (th . shift 1)
public export public export
drop1 : Subst f (S from) to -> Subst f from to drop1 : Subst f (S from) to -> Subst f from to
drop1 (Shift by) = Shift $ drop1 by drop1 (Shift by) = Shift $ ssDown by
drop1 (t ::: th) = th drop1 (t ::: th) = th