git.iko.soy/Idris-dev
on master help sign in
Add where keyword to UList and BadList in the Uniqueness Types documentation.
9c5b561michaelmcgirr
docs/reference/uniqueness-types.rst+2−2
compare with master
unifiedsplit
@@ -34,7 +34,7 @@ declare the type of unique lists as follows:
34
34
35.. code-block:: idris
35.. code-block:: idris
36
36
37− data UList : Type -> UniqueType
37+ data UList : Type -> UniqueType where
38 Nil : UList a
38 Nil : UList a
39 (::) : a -> UList a -> UList a
39 (::) : a -> UList a -> UList a
40
40
@@ -94,7 +94,7 @@ since it would embed a unique value in a possible non-unique value:
94
94
95.. code-block:: idris
95.. code-block:: idris
96
96
97− data BadList : UniqueType -> Type
97+ data BadList : UniqueType -> Type where
98 Nil : {a : UniqueType} -> BadList a
98 Nil : {a : UniqueType} -> BadList a
99 (::) : {a : UniqueType} -> a -> BadList a -> BadList a
99 (::) : {a : UniqueType} -> a -> BadList a -> BadList a
100
100