git.iko.soy/Idris-dev
on 4c19d46 help sign in
Idris-dev/test/docs001/docs001.idr
20 lines 309 B history raw
1||| interface
2||| @ t a type
3interface C (t : Type) where
4 ||| member of interface
5 m : t
7||| type
8data A = B
10||| type 2
11data D a b = E
13||| implementation of interface
14implementation C A where
15 m = B
17||| another implementation of interface
18||| @ a parameter type
19implementation C (D a b) where
20 m = E