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