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
|
File "stdin", line 10, characters 0-28:
Warning:
New coercion path [ac; cd] : A >-> D is ambiguous with existing
[ab; bd] : A >-> D. [ambiguous-paths,typechecker]
[ab] : A >-> B
[ab; bd] : A >-> D
[ac] : A >-> C
[bd] : B >-> D
[cd] : C >-> D
File "stdin", line 26, characters 0-28:
Warning:
New coercion path [ab; bc] : A >-> C is ambiguous with existing
[ac] : A >-> C. [ambiguous-paths,typechecker]
[ac] : A >-> C
[ac; cd] : A >-> D
[ab] : A >-> B
[cd] : C >-> D
[bc] : B >-> C
[bc; cd] : B >-> D
[B_A] : B >-> A
[C_A] : C >-> A
[D_B] : D >-> B
[D_A] : D >-> A
[D_C] : D >-> C
[A'_A] : A' >-> A
[B_A'] : B >-> A'
[B_A'; A'_A] : B >-> A
[C_A'] : C >-> A'
[C_A'; A'_A] : C >-> A
[D_B; B_A'] : D >-> A'
[D_A] : D >-> A
[D_B] : D >-> B
[D_C] : D >-> C
File "stdin", line 121, characters 0-86:
Warning:
New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
[D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker]
[A'_A] : A' >-> A
[B_A'] : B >-> A'
[B_A'; A'_A] : B >-> A
[C_A'] : C >-> A'
[C_A'; A'_A] : C >-> A
[D_B; B_A'] : D >-> A'
[D_A] : D >-> A
[D_B] : D >-> B
[D_C] : D >-> C
File "stdin", line 130, characters 0-47:
Warning:
New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT is not definitionally an identity function.
[ambiguous-paths,typechecker]
File "stdin", line 131, characters 0-64:
Warning:
New coercion path [unwrap_list; wrap_list] : LIST >-> LIST is not definitionally an identity function.
[ambiguous-paths,typechecker]
File "stdin", line 132, characters 0-51:
Warning:
New coercion path [unwrap_Type; wrap_Type] : TYPE >-> TYPE is not definitionally an identity function.
[ambiguous-paths,typechecker]
|
