git.iko.soy/Idris-dev
on 89c19be help sign in
Idris-dev/test/docs004/expected
15 lines 316 B history raw
1MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a
2 Constructor for Foo
3 Arguments:
4 (implicit) a : Type -- a type
5
6 bar : Nat -- A field bar
7
8 baz : Bool -- A field baz
9
10bar : (rec : Foo a) -> Nat
11 A field bar
13baz : (rec : Foo a) -> Bool
14 A field baz