packages feed

idris-0.12.1: test/records004/records004.idr

-- Test for multiple field declarations on one line with the same type

record Person where
  constructor MkPerson
  firstName, middleName, lastName : String

fred : Person
fred = MkPerson "Fred" "Joe" "Bloggs"

main : IO ()
main = do printLn (firstName fred)
          printLn (middleName fred)
          printLn (lastName fred)