git.iko.soy/Idris-dev
on master help sign in
corrected wrong type signature in definition of 'so' in tutorial.
0215302Mekeor Melire
tutorial/typesfuns.tex+1−1
compare with master
unifiedsplit
@@ -869,7 +869,7 @@ value is true:
869
869
870\begin{SaveVerbatim}{sotype}
870\begin{SaveVerbatim}{sotype}
871
871
872−data so : Bool where
872+data so : Bool -> Set where
873 oh : so True
873 oh : so True
874
874
875\end{SaveVerbatim}
875\end{SaveVerbatim}