@@ -34,7 +34,7 @@ declare the type of unique lists as follows:
35.. code-block:: idris
35.. code-block:: idris
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
@@ -94,7 +94,7 @@ since it would embed a unique value in a possible non-unique value:
95.. code-block:: idris
95.. code-block:: idris
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