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

fiddling

Browse source
This commit is contained in:
rhiannon morris 2022-04-11 23:34:18 +02:00
parent 25f4923fac
commit d912614d7d
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Quox/Context.idr
View file

@ -37,25 +37,25 @@ Context' a = Context (\_ => a)
export export
toSnocList : Telescope {tm, _} -> SnocList (Exists tm) toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
toSnocList [<] = [<] toSnocList [<] = [<]
toSnocList (tel :< t) = toSnocList tel :< Evidence _ t toSnocList (tel :< t) = toSnocList tel :< Evidence _ t
private private
toListAcc : Telescope {tm, _} -> List (Exists tm) -> List (Exists tm) toListAcc : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
toListAcc [<] acc = acc toListAcc [<] acc = acc
toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc) toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc)
export %inline export %inline
toList : Telescope {tm, _} -> List (Exists tm) toList : Telescope tm _ _ -> List (Exists tm)
toList tel = toListAcc tel [] toList tel = toListAcc tel []
export %inline export %inline
toSnocList' : Telescope' {a, _} -> SnocList a toSnocList' : Telescope' a _ _ -> SnocList a
toSnocList' = map snd . toSnocList toSnocList' = map snd . toSnocList
export %inline export %inline
toList' : Telescope' {a, _} -> List a toList' : Telescope' a _ _ -> List a
toList' = map snd . toList toList' = map snd . toList