Merge pull request #28 from MekeorMelire/master
Mistake in tutorial
commit72a8ac49ad117fe95494c890111084de7914c5d4
authorEdwin Brady <edwin.brady@gmail.com>
dateThu 31 May 2012, 03:42 (14 years ago)
parent2ec60c80215302
tutorial/typesfuns.tex+1−1
@@ -869,7 +869,7 @@ value is true:
869869
870870\begin{SaveVerbatim}{sotype}
871871
872−data so : Bool where
872+data so : Bool -> Set where
873873 oh : so True
874874
875875\end{SaveVerbatim}