Alias.hascasl.output revision 33a5d53a412ba0a4e5847f7538d6da2e22bd116c
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
var s : Type
type MyPred : Type -> Type := \ s : Type . s ->? Unit
type MyAlias : Type -> Type := \ t : Type . t ->? Unit
type a1 : Type -> Type -> Type := \ (a : Type)
(b : Type) . a -> b -> Unit
type a1 : Type -> Type -> Type := \ (a : Type)
(b : Type) . a -> b -> Unit
type a1 : Type -> Type -> Type := \ (a : Type)
(b : Type) . a -> b -> Unit
type a2 : Type -> Type -> Type := \ (a : Type)
(b : Type) . a -> Unit
type a3 : Type -> Type -> Type := \ (a : Type)
(a : Type) . a -> Unit
type a4 : Type -> Type -> Type := \ (a : Type)
(a : Type) . a -> Unit
type a5(a : Type)
type a5 : Type -> Type := \ a : Type . a5 a -> Unit
type a6(a : Type)
type a7 : Type -> Type := \ a : Type . a6 a -> Unit
type a6 : Type -> Type := \ a : Type . (a6 a -> Unit) -> Unit
%% Type Constructors -----------------------------------------------------
MyAlias : Type -> Type := \ t : Type . t ->? Unit
MyPred : Type -> Type := \ s : Type . s ->? Unit
Pred : Type -> Type := \ a : Type . a ->? Unit
Unit : Type := Unit
__-->__ : Type- -> Type+ -> Type
__-->?__ : Type- -> Type+ -> Type
__->__ : Type- -> Type+ -> Type
__->?__ : Type- -> Type+ -> Type
__�__ : Type+ -> Type+ -> Type
a1 : Type -> Type -> Type := \ (a : Type)
(b : Type) . a -> b -> Unit
a2 : Type -> Type -> Type := \ (a : Type)(b : Type) . a -> Unit
a3 : Type -> Type -> Type := \ (a : Type)(a : Type) . a -> Unit
a4 : Type -> Type -> Type := \ (a : Type)(a : Type) . a -> Unit
a5 : Type -> Type
a6 : Type -> Type
a7 : Type -> Type := \ a : Type . a6 a -> Unit
s : Type %(var)%
%% Assumptions -----------------------------------------------------------
__/\__ : Unit � Unit ->? Unit
__<=>__ : Unit � Unit ->? Unit
__=__ : forall a : Type . a � a ->? Unit
__=>__ : Unit � Unit ->? Unit
__=e=__ : forall a : Type . a � a ->? Unit
__\/__ : Unit � Unit ->? Unit
def__ : forall a : Type . a ->? Unit
if__then__else__ : forall a : Type . Unit � a � a ->? a
not__ : Unit ->? Unit
%% Diagnostics -----------------------------------------------------------
Hint (line 1, column 5) is type variable 's'
Warning (line 6, column 6) redeclared type 'a1'
Warning (line 7, column 6) redeclared type 'a1'
Warning (line 11, column 19) redeclared type 'a'
Error (line 11, column 15) duplicates at '(11,19)' for 'a'
Error (line 13, column 9) duplicates at '(13,11)' for 'a'
Error (line 17, column 14) illegal recursive type synonym 'a5 a -> Unit'
Error (line 21, column 14) illegal recursive type synonym '(a6 a -> Unit) -> Unit'