diff options
Diffstat (limited to 'src/Encoded/Vect.idr')
| -rw-r--r-- | src/Encoded/Vect.idr | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/Encoded/Vect.idr b/src/Encoded/Vect.idr index a427196..064de5f 100644 --- a/src/Encoded/Vect.idr +++ b/src/Encoded/Vect.idr @@ -6,7 +6,6 @@ import Encoded.Bool import Encoded.Pair import Encoded.Fin -import Term.Semantics import Term.Syntax export @@ -14,13 +13,6 @@ Vect : Nat -> Ty -> Ty Vect k ty = Fin k ~> ty export -[ShowVect] -{k : Nat} -> -Show (TypeOf ty) => -Show (TypeOf (Vect k ty)) where - show f = "[" ++ joinBy ", " (map (show . f) $ allSem k) ++ "]" - -export nil : {ty : Ty} -> Term (Vect 0 ty) ctx nil = absurd |