The old code doesn't work
The type of SizedClass.set_students is Vect size Person -> SizedClass size -> SizedClass size, so this function must use the constructor SizedClassInfo.
commit2cfbee407ec9e8695cad26ad57b25326da706145
authorChao-Hong Chen <dreamlinuxer@gmail.com>
dateTue 5 Jan 2016, 22:50 (11 years ago)
parent79ff02f
docs/tutorial/typesfuns.rst+1−1
@@ -1045,7 +1045,7 @@ using natural numbers, the new value can be incremented using the
10451045.. code-block:: idris
10461046
10471047 addStudent : Person -> SizedClass n -> SizedClass (S n)
1048− addStudent p c = record { students = p :: students c } c
1048+ addStudent p c = SizedClassInfo (p :: students c) (className c)
10491049
10501050.. _sect-more-expr:
10511051