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

Show Telescope

Browse source
This commit is contained in:
rhiannon morris 2023-03-13 18:25:07 +01:00
parent c81aabcc14
commit 8e9b0abb34
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
lib/Quox/Context.idr
View file

@ -221,6 +221,11 @@ export %inline
(forall n. Ord (tm n)) => Ord (Telescope tm from to) where (forall n. Ord (tm n)) => Ord (Telescope tm from to) where
compare = foldLazy .: zipWithLazy compare compare = foldLazy .: zipWithLazy compare
export %inline
(forall n. Show (tm n)) => Show (Telescope tm from to) where
showPrec d = showPrec d . toSnocList
where Show (Exists tm) where showPrec d t = showPrec d t.snd
export %inline export %inline
(forall n. PrettyHL (tm n)) => PrettyHL (Telescope tm from to) where (forall n. PrettyHL (tm n)) => PrettyHL (Telescope tm from to) where
prettyM tel = separate (hl Delim ";") <$> traverse prettyM (toList tel) prettyM tel = separate (hl Delim ";") <$> traverse prettyM (toList tel)