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

add Context.unzip

Browse source
This commit is contained in:
rhiannon morris 2023-02-11 18:13:44 +01:00
parent 42798f243f
commit 8de5803cba
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
lib/Quox/Context.idr
View file

@ -215,6 +215,13 @@ zipWith3Lazy : forall tm1, tm2, tm3, tm4.
zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
export
unzip : Telescope (\i => (tm1 i, tm2 i)) from to ->
(Telescope tm1 from to, Telescope tm2 from to)
unzip [<] = ([<], [<])
unzip (tel :< (x, y)) = let (xs, ys) = unzip tel in (xs :< x, ys :< y)
export
lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
lengthPrf [<] = Element 0 Refl