corrected wrong type signature in definition of 'so' in tutorial.
commit021530249590ce3ac4528d2bebed5f1c8edd80b1
authorMekeor Melire <mekeor@ymail.com>
dateWed 16 May 2012, 19:05 (14 years ago)
parent541faf5
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}