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