git.iko.soy/Idris-dev
on 33166ee help sign in
Idris-dev/test/classes001/expected
29 lines 722 B history raw
1Interface MyShow
2 A fancy shower with a constructor
4Parameters:
5 a -- the thing to be shown
7Methods:
8 myShow : MyShow a => (x : a) -> String
9 The shower
11 The function is Total
12Implementation constructor:
13 MkMyShow : (myShow : a -> String) -> MyShow a
14 Build a MyShow
15 Arguments:
16 (implicit) a : Type -- the thing to be shown
18 myShow : a -> String -- The shower
20Implementations:
21 MyShow Integer
22MkMyShow : (myShow : a -> String) -> MyShow a
23 Build a MyShow
24 Arguments:
25 (implicit) a : Type -- the thing to be shown
27 myShow : a -> String -- The shower
29 The function is Total