@@ -34,7 +34,7 @@ declare the type of unique lists as follows:
3434
3535.. code-block:: idris
3636
37− data UList : Type -> UniqueType
37+ data UList : Type -> UniqueType where
3838 Nil : UList a
3939 (::) : a -> UList a -> UList a
4040
@@ -94,7 +94,7 @@ since it would embed a unique value in a possible non-unique value:
9494
9595.. code-block:: idris
9696
97− data BadList : UniqueType -> Type
97+ data BadList : UniqueType -> Type where
9898 Nil : {a : UniqueType} -> BadList a
9999 (::) : {a : UniqueType} -> a -> BadList a -> BadList a
100100