summaryrefslogtreecommitdiff
path: root/transfer
diff options
context:
space:
mode:
Diffstat (limited to 'transfer')
-rw-r--r--transfer/lib/prelude.tr2
1 files changed, 1 insertions, 1 deletions
diff --git a/transfer/lib/prelude.tr b/transfer/lib/prelude.tr
index a9ec4812b..3ec830d13 100644
--- a/transfer/lib/prelude.tr
+++ b/transfer/lib/prelude.tr
@@ -122,7 +122,7 @@ mul_Bool = rec one = True
-- The List type
--
-data List : (_:Type) -> Type where
+data List : Type -> Type where
Nil : (A:Type) -> List A
Cons : (A:Type) -> A -> List A -> List A