Foldl.hascasl.output revision 4d5d65e4f55ba8eaa02a4dab14348abeda75cf6b
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
var a : Type
type List(a : Type)
op nil : List a
op head : List a -> a
op snoc : List a -> a --> List a
forall x : a
. ((fun __=__[List a] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
List a * List a ->? Unit)
((((op snoc[a]
: forall a : Type . List a_v-1 -> a_v-1 --> List a_v-1) :
List a -> a --> List a)
((op nil[a] : forall a : Type . List a_v-1) : List a) :
a --> List a)
(var x : a) :
List a,
(((op snoc[a]
: forall a : Type . List a_v-1 -> a_v-1 --> List a_v-1) :
List a -> a --> List a)
((op nil[a] : forall a : Type . List a_v-1) : List a) :
a --> List a)
(var x : a) :
List a) :
Unit
. ((fun __=__[a] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
a * a ->? Unit)
((((op head[a ->? a] : forall a : Type . List a_v-1 -> a_v-1) :
List (a ->? a) -> a ->? a)
((op nil[a ->? a] : forall a : Type . List a_v-1) :
List (a ->? a)) :
a ->? a)
(var x : a) :
a,
var x : a) :
Unit
%% Type Constructors -----------------------------------------------------
List : Type -> Type
Logical : Type := Unit ->? Unit
Pred : Type -> Type := \ a : Type . a_v-1 ->? Unit
Unit : Type
__*__ : +Type -> +Type -> Type
__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)
__-->?__ : -Type -> +Type -> Type < __->?__
__->__ : -Type -> +Type -> Type < __->?__
__->?__ : -Type -> +Type -> Type
a : Type %(var_1)%
%% Assumptions -----------------------------------------------------------
__/\__ : ? Unit * ? Unit ->? Unit %(fun)%
__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__\/__ : ? Unit * ? Unit ->? Unit %(fun)%
__if__ : ? Unit * ? Unit ->? Unit %(fun)%
__when__else__
: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%
bottom : forall a : Type . a_v-1 %(fun)%
def__ : forall a : Type . a_v-1 ->? Unit %(fun)%
false : Unit %(fun)%
head : forall a : Type . List a_v-1 -> a_v-1 %(op)%
nil : forall a : Type . List a_v-1 %(op)%
not__ : ? Unit ->? Unit %(fun)%
snoc : forall a : Type . List a_v-1 -> a_v-1 --> List a_v-1 %(op)%
true : Unit %(fun)%
�__ : ? Unit ->? Unit %(fun)%
%% Sentences -------------------------------------------------------------
((fun __=__[List a] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
List a * List a ->? Unit)
((((op snoc[a]
: forall a : Type . List a_v-1 -> a_v-1 --> List a_v-1) :
List a -> a --> List a)
((op nil[a] : forall a : Type . List a_v-1) : List a) :
a --> List a)
(var x : a) :
List a,
(((op snoc[a]
: forall a : Type . List a_v-1 -> a_v-1 --> List a_v-1) :
List a -> a --> List a)
((op nil[a] : forall a : Type . List a_v-1) : List a) :
a --> List a)
(var x : a) :
List a) :
Unit
((fun __=__[a] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
a * a ->? Unit)
((((op head[a ->? a] : forall a : Type . List a_v-1 -> a_v-1) :
List (a ->? a) -> a ->? a)
((op nil[a ->? a] : forall a : Type . List a_v-1) :
List (a ->? a)) :
a ->? a)
(var x : a) :
a,
var x : a) :
Unit
%% Diagnostics -----------------------------------------------------------
*** Hint 1.5, is type variable 'a'
*** Hint 6.9, not a class 'a'