forked from GitHub/gf-core
Removed variable for the type argument of List.
This commit is contained in:
@@ -122,7 +122,7 @@ mul_Bool = rec one = True
|
|||||||
-- The List type
|
-- The List type
|
||||||
--
|
--
|
||||||
|
|
||||||
data List : (_:Type) -> Type where
|
data List : Type -> Type where
|
||||||
Nil : (A:Type) -> List A
|
Nil : (A:Type) -> List A
|
||||||
Cons : (A:Type) -> A -> List A -> List A
|
Cons : (A:Type) -> A -> List A -> List A
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user