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

add DimEqs.get etc

Browse source
This commit is contained in:
rhiannon morris 2022-02-27 01:33:52 +01:00
parent 8006ae4c40
commit 610b5fde2d
1 changed files with 14 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Quox/Syntax/DimEq.idr
View file

@ -39,10 +39,22 @@ new : (d : Nat) -> DimEq d
new d = C (new' d)
export
private %inline
shiftMay : Maybe (Dim from) -> Shift from to -> Maybe (Dim to)
shiftMay p by = map (// by) p
export %inline
get' : DimEq' d -> Var d -> Maybe (Dim d)
get' = getWith shiftMay
private %inline
getShift' : Shift len out -> DimEq' len -> Var len -> Maybe (Dim out)
getShift' = getShiftWith shiftMay
export %inline
get : DimEq' d -> Dim d -> Dim d
get _ (K e) = K e
get eqs (B i) = fromMaybe (B i) $ (eqs !! i) @{Compose}
get eqs (B i) = fromMaybe (B i) $ get' eqs i
export %inline