Fix some strings that were messed up by the initial Idris -> Newt perl code
This commit is contained in:
@@ -23,7 +23,7 @@ data Binder : U where
|
||||
-- I don't have a show for terms without a name list
|
||||
|
||||
instance Show Binder where
|
||||
show (MkBinder _ nm icit quant t) = "(\{show quant}\{nm} \{show icit} : ... :: Nil)"
|
||||
show (MkBinder _ nm icit quant t) = "[\{show quant}\{nm} \{show icit} : ...]"
|
||||
|
||||
splitTele : Tm -> (Tm × List Binder)
|
||||
splitTele = go Nil
|
||||
|
||||
Reference in New Issue
Block a user