git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/test/docs004/docs004.idr
11 lines 173 B history raw
1module Main
3||| Some record Foo
4||| @a a type
5record Foo a where
6 ||| Constructor for Foo
7 constructor MkFoo
8 ||| A field bar
9 bar : Nat
10 ||| A field baz
11 baz : Bool