Merge pull request #2885 from DreamLinuxer/patch-1
The old code doesn't work
commit2f5dd7995467cd5f7b09e8e0ce24fa0c07998b61
authorEdwin Brady <edwin.brady@gmail.com>
dateWed 20 Jan 2016, 16:04 (11 years ago)
parenta356ee82cfbee4
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