git.iko.soy/Idris-dev
on master help sign in
Merge pull request #28 from MekeorMelire/master
72a8ac4Edwin Brady
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}