Fixes error in type definition for So.
The type definition for So used the syntax:
```
data So : Bool -> Type = Oh : So True
```
which is not valid idris.
Fixes https://github.com/idris-lang/Idris-dev/issues/4683
commit7c7a17a92c83f82a8f0afe48616e477ad3b159b1
authorIvan Perez <ivan.perez@keera.co.uk>
dateMon 1 Apr 2019, 15:05 (8 years ago)
parent268db5d
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