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

those were not meant to stay there

Browse source
This commit is contained in:
rhiannon morris 2023-05-21 20:10:09 +02:00
parent 42aa07c9c8
commit 2af8ee20ea
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
lib/Quox/Syntax/Term/Pretty.idr
View file

@ -221,9 +221,6 @@ where
go (Left p :: xs) $ assert_smaller e $ pushSubsts' f
go xs s = (s, xs)
export FromString (Elim d n) where fromString s = F (fromString s) noLoc
export FromString (Term d n) where fromString s = FT (fromString s) noLoc
private
prettyDTApps : {opts : _} ->
BContext d -> BContext n ->