Merge pull request #4684 from ivanperez-keera/master
Fixes error in type definition for So.
commitaee9c52414cee2f800e47ceebb3877eb5d6edc4f
authorNiklas Larsson <metaniklas@gmail.com>
dateMon 1 Apr 2019, 23:58 (8 years ago)
parent268db5d7c7a17a
docs/effects/simpleeff.rst+2−1
@@ -212,7 +212,8 @@ from the result of a dynamic check:
212212
213213.. code-block:: idris
214214
215− data So : Bool -> Type = Oh : So True
215+ data So : Bool -> Type where
216+ Oh : So True
216217
217218 choose : (b : Bool) -> Either (So b) (So (not b))
218219