git.iko.soy/Idris-dev
on master help sign in
Idris-dev/samples/tutorial/Record.idr
21 lines 463 B history raw
1import Data.Vect
3record Person where
4 constructor MkPerson
5 firstName, middleName, lastName : String
6 age : Int
8fred : Person
9fred = MkPerson "Fred" "Joe" "Bloggs" 30
11record Class where
12 constructor ClassInfo
13 students : Vect n Person
14 className : String
16addStudent : Person -> Class -> Class
17addStudent p c = record { students = p :: students c } c
19addStudent' : Person -> Class -> Class
20addStudent' p c = record { students $= (p ::) } c