git.iko.soy/Idris-dev
on master help sign in
Instance docs: simplify test case
75bf0d8Adam Sandberg Eriksson
test/interactive008/expected+5−4
compare with master
unifiedsplit
@@ -1,14 +1,15 @@
1+Type checking ./interactive008.idr
1*interactive008> Type class C
2*interactive008> Type class C
2 class
3 class
3
4
4Parameters:
5Parameters:
5− t
6+ t -- a type
6
7
7Methods:
8Methods:
8− f : C t => t
9+ m : C t => t
9− member
10+ member of class
10
11
11Instances:
12Instances:
12 C A
13 C A
13− instance
14+ instance of class
14*interactive008> Bye bye
15*interactive008> Bye bye
test/interactive008/interactive008.idr+6−7
@@ -1,13 +1,12 @@
1−
2||| class
1||| class
2+||| @ t a type
3class C (t : Type) where
3class C (t : Type) where
4− ||| member
4+ ||| member of class
5− f : t
5+ m : t
6
6
7||| type
7||| type
8−data A : Type where
8+data A = B
9− i : A
10
9
11−||| instance
10+||| instance of class
12instance C A where
11instance C A where
13− f = i
12+ m = B