@@ -212,7 +212,8 @@ from the result of a dynamic check:
213.. code-block:: idris
213.. code-block:: idris
215− data So : Bool -> Type = Oh : So True
215+ data So : Bool -> Type where
217 choose : (b : Bool) -> Either (So b) (So (not b))
218 choose : (b : Bool) -> Either (So b) (So (not b))