git.iko.soy/Idris-dev
on 8fe28aa help sign in
Idris-dev/test/docs004/expected
18 lines 468 B history raw
1Main.MkFoo : (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
10 The function is: Total & public export
11Main.Foo.bar : (rec : Foo a) -> Nat
12 A field bar
14 The function is: Total & public export
15Main.Foo.baz : (rec : Foo a) -> Bool
16 A field baz
18 The function is: Total & public export