@@ -1045,7 +1045,7 @@ using natural numbers, the new value can be incremented using the
1045.. code-block:: idris
1045.. code-block:: idris
1047 addStudent : Person -> SizedClass n -> SizedClass (S n)
1047 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)
1050.. _sect-more-expr:
1050.. _sect-more-expr: