git.iko.soy/Idris-dev
on dbf060c help sign in
Idris-dev/test/docs005/expected
31 lines 909 B history raw
1Data type docs005.Foobar : Type
2 A foobar with an auto implicit
3
4 The function is: public export
5Constructors:
6 NewFoo : (xs : List String) ->
7 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
8 New Foo
9 Arguments:
10 xs : List String -- Some xs
12 ys : List Nat -- Some ys
14 (implicit) prf1 : NonEmpty xs -- A prf
16 (auto implicit) prf : NonEmpty ys -- The prf
18 The function is: public export
19docs005.NewFoo : (xs : List String) ->
20 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
21 New Foo
22 Arguments:
23 xs : List String -- Some xs
25 ys : List Nat -- Some ys
27 (implicit) prf1 : NonEmpty xs -- A prf
29 (auto implicit) prf : NonEmpty ys -- The prf
31 The function is: Total & public export