From d912614d7de593a58797b9929a74fd27f3d19540 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 11 Apr 2022 23:34:18 +0200 Subject: [PATCH] fiddling --- src/Quox/Context.idr | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr index 20875d1..6a058c7 100644 --- a/src/Quox/Context.idr +++ b/src/Quox/Context.idr @@ -37,25 +37,25 @@ Context' a = Context (\_ => a) export -toSnocList : Telescope {tm, _} -> SnocList (Exists tm) +toSnocList : Telescope tm _ _ -> SnocList (Exists tm) toSnocList [<] = [<] toSnocList (tel :< t) = toSnocList tel :< Evidence _ t private -toListAcc : Telescope {tm, _} -> List (Exists tm) -> List (Exists tm) +toListAcc : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm) toListAcc [<] acc = acc toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc) export %inline -toList : Telescope {tm, _} -> List (Exists tm) +toList : Telescope tm _ _ -> List (Exists tm) toList tel = toListAcc tel [] export %inline -toSnocList' : Telescope' {a, _} -> SnocList a +toSnocList' : Telescope' a _ _ -> SnocList a toSnocList' = map snd . toSnocList export %inline -toList' : Telescope' {a, _} -> List a +toList' : Telescope' a _ _ -> List a toList' = map snd . toList