test011.idr

module Main

record Foo : Nat -> Type where
    MkFoo : (name : String) ->
            (things : Vect n a) ->
            (more_things : Vect m b) ->
            Foo n

record Person : Type where
    MkPerson : (name : String) -> (age : Int) -> Person

testFoo : Foo 3
testFoo = MkFoo "name" [1,2,3] [4,5,6,7]

person : Person
person = MkPerson "Fred" 30

main : IO ()
main = do let x = record { name = "foo",
                           more_things = reverse ["a","b"] } testFoo
          print $ name x
          print $ name person
          print $ things x
          print $ more_things x
          print $ age (record { age = 25 } person)