git.iko.soy/Idris-dev
on e8596bc help sign in
Idris-dev/test/docs005/docs005.idr
19 lines 350 B history raw
1module docs005
3import Data.List
5%default total
7||| A foobar with an auto implicit
8data Foobar : Type where
9 ||| New Foo
10 |||
11 ||| @xs Some `xs`
12 ||| @ys Some `ys`
13 ||| @prf The prf
14 ||| @prf1 A prf
15 NewFoo : (xs : List String)
16 -> (ys : List Nat)
17 -> {prf1 : NonEmpty xs}
18 -> {auto prf : NonEmpty ys}
19 -> Foobar