Quelle  NumberNotations.out   Sprache: unbekannt

File "./output/NumberNotations.v", line 11, characters 13-14:
The command has indeed failed with message:
Unexpected term (nat -> nat) while parsing a number notation.
File "./output/NumberNotations.v", line 21, characters 13-14:
The command has indeed failed with message:
Unexpected non-option term opaque4 while parsing a number notation.
File "./output/NumberNotations.v", line 32, characters 13-14:
The command has indeed failed with message:
Unexpected term (fun (A : Type) (x : A) => x) while parsing a number
notation.
let v := 0%ppp in v : punit
     : punit
let v := 0%ppp in v : punit
     : punit
let v := 0%ppp in v : punit
     : punit
let v := 0%ppp in v : punit
     : punit
let v := 0%uto in v : unit
     : unit
File "./output/NumberNotations.v", line 72, characters 13-14:
The command has indeed failed with message:
Cannot interpret this number as a value of type unit
File "./output/NumberNotations.v", line 73, characters 14-16:
The command has indeed failed with message:
Cannot interpret this number as a value of type unit
let v := 0%upp in v : unit
     : unit
let v := 0%upp in v : unit
     : unit
let v := 0%upp in v : unit
     : unit
let v := 0%ppps in v : punit
     : punit
File "./output/NumberNotations.v", line 91, characters 2-46:
Warning: To avoid stack overflow, large numbers in punit are interpreted as
applications of pto_punits. [abstract-large-number,numbers,default]
File "./output/NumberNotations.v", line 91, characters 32-33:
The command has indeed failed with message:
In environment
v := pto_punits (Number.UIntDecimal (Decimal.D1 Decimal.Nil)) : punit
The term "v" has type "punit@{Set}" while it is expected to have type
 "punit@{u}"
(universe inconsistency: Cannot enforce Set = u).
S
     : nat -> nat
S (ack 4 4)
     : nat
let v := 0%wnat in v : wnat
     : wnat
0%wnat
     : wnat
{| unwrap := ack 4 4 |}
     : wnat
{| Test6.unwrap := 0 |}
     : Test6.wnat
let v := 0%wnat in v : Test6.wnat
     : Test6.wnat
let v := 0%wuint in v : wuint
     : wuint
let v := 1%wuint in v : wuint
     : wuint
let v := 0%wuint8 in v : wuint
     : wuint
let v := 0 in v : nat
     : nat
File "./output/NumberNotations.v", line 164, characters 34-35:
The command has indeed failed with message:
In environment
v := 0 : nat
The term "v" has type "nat" while it is expected to have type "wuint".
     = {| unwrap := Number.UIntDecimal (Decimal.D0 Decimal.Nil) |}
     : wuint
let v := 0%wuint8' in v : wuint
     : wuint
let v := 0%wuint9 in v : wuint
     : wuint
let v := 0%wuint9' in v : wuint
     : wuint
let v := 0 in v : nat
     : nat
File "./output/NumberNotations.v", line 191, characters 34-35:
The command has indeed failed with message:
In environment
v := 0 : nat
The term "v" has type "nat" while it is expected to have type "wuint".
File "./output/NumberNotations.v", line 203, characters 2-71:
Warning: The 'abstract after' directive has no effect when the parsing
function (of_uint) targets an option type.
[abstract-large-number-no-op,numbers,default]
File "./output/NumberNotations.v", line 206, characters 2-77:
The command has indeed failed with message:
The 'abstract after' directive has no effect when the parsing function
(of_uint) targets an option type.
[abstract-large-number-no-op,numbers,default]
let v := of_uint (Number.UIntDecimal (Decimal.D1 Decimal.Nil)) in v : unit
     : unit
let v := 0%test13 in v : unit
     : unit
File "./output/NumberNotations.v", line 238, characters 36-44:
The command has indeed failed with message:
to_uint' is bound to a notation that does not denote a reference.
File "./output/NumberNotations.v", line 239, characters 35-36:
The command has indeed failed with message:
In environment
v := 0 : nat
The term "v" has type "nat" while it is expected to have type "unit".
File "./output/NumberNotations.v", line 240, characters 36-45:
The command has indeed failed with message:
to_uint'' is bound to a notation that does not denote a reference.
File "./output/NumberNotations.v", line 241, characters 36-37:
The command has indeed failed with message:
In environment
v := 0 : nat
The term "v" has type "nat" while it is expected to have type "unit".
let v := 0%test14' in v : unit
     : unit
let v := 0%test14' in v : unit
     : unit
File "./output/NumberNotations.v", line 264, characters 34-35:
The command has indeed failed with message:
In environment
v := 0 : nat
The term "v" has type "nat" while it is expected to have type "unit".
File "./output/NumberNotations.v", line 265, characters 35-36:
The command has indeed failed with message:
In environment
v := 0 : nat
The term "v" has type "nat" while it is expected to have type "unit".
File "./output/NumberNotations.v", line 267, characters 34-35:
The command has indeed failed with message:
In environment
v := 0 : nat
The term "v" has type "nat" while it is expected to have type "unit".
let v := 0%test14' in v : unit
     : unit
File "./output/NumberNotations.v", line 273, characters 4-71:
The command has indeed failed with message:
This command does not support the Global option in sections.
let v := 0%test14'' in v : unit
     : unit
File "./output/NumberNotations.v", line 275, characters 39-40:
The command has indeed failed with message:
In environment
v := 0 : nat
The term "v" has type "nat" while it is expected to have type "unit".
File "./output/NumberNotations.v", line 277, characters 36-37:
The command has indeed failed with message:
In environment
v := 0 : nat
The term "v" has type "nat" while it is expected to have type "unit".
File "./output/NumberNotations.v", line 278, characters 37-38:
The command has indeed failed with message:
In environment
v := 0 : nat
The term "v" has type "nat" while it is expected to have type "unit".
let v := 0%test15 in v : unit
     : unit
let v := 0%test15 in v : unit
     : unit
let v := 0%test15 in v : unit
     : unit
let v := foo a.t in v : Foo
     : Foo
File "./output/NumberNotations.v", line 320, characters 22-23:
The command has indeed failed with message:
Cannot interpret in test16_scope because NumberNotations.Test16.F.Foo could not be found in the current environment.
let v := 0%test17 in v : myint63
     : myint63
let v := 0%Q in v : Q
     : Q
let v := 1%Q in v : Q
     : Q
let v := 2%Q in v : Q
     : Q
let v := 3%Q in v : Q
     : Q
let v := 4%Q in v : Q
     : Q
     = (0, 1)
     : nat * nat
     = (1, 1)
     : nat * nat
     = (2, 1)
     : nat * nat
     = (3, 1)
     : nat * nat
     = (4, 1)
     : nat * nat
let v := (-1)%Zlike in v : Zlike
     : Zlike
let v := 0%Zlike in v : Zlike
     : Zlike
let v := 1%Zlike in v : Zlike
     : Zlike
let v := 2%Zlike in v : Zlike
     : Zlike
let v := 3%Zlike in v : Zlike
     : Zlike
let v := 4%Zlike in v : Zlike
     : Zlike
2%Zlike
     : Zlike
0%Zlike
     : Zlike
let v := 0%kt in v : ty
     : ty
let v := 1%kt in v : ty
     : ty
let v := 2%kt in v : ty
     : ty
let v := 3%kt in v : ty
     : ty
let v := 4%kt in v : ty
     : ty
let v := 5%kt in v : ty
     : ty
File "./output/NumberNotations.v", line 463, characters 22-23:
The command has indeed failed with message:
Cannot interpret this number as a value of type ty
     = 0%kt
     : ty
     = 1%kt
     : ty
     = 2%kt
     : ty
     = 3%kt
     : ty
     = 4%kt
     : ty
     = 5%kt
     : ty
let v : ty := Build_ty Empty_set zero in v : ty
     : ty
let v : ty := Build_ty unit one in v : ty
     : ty
let v : ty := Build_ty bool two in v : ty
     : ty
let v : ty := Build_ty Prop prop in v : ty
     : ty
let v : ty := Build_ty Set set in v : ty
     : ty
let v : ty := Build_ty Type type in v : ty
     : ty
1
     : nat
1000
     : nat
0
     : Prop
+0
     : bool
-0
     : bool
00
     : nat * nat
1000
     : Prop
1_000
     : list nat
0
     : Set
1
     : Set
2
     : Set
3
     : Set
Empty_set
     : Set
unit
     : Set
sum unit unit
     : Set
sum unit (sum unit unit)
     : Set
File "./output/NumberNotations.v", line 558, characters 0-112:
The command has indeed failed with message:
Missing mapping for constructor Isum.
File "./output/NumberNotations.v", line 564, characters 68-73:
The command has indeed failed with message:
Iunit was already mapped to unit and cannot be remapped to unit.
File "./output/NumberNotations.v", line 568, characters 47-50:
The command has indeed failed with message:
add is not an inductive type.
File "./output/NumberNotations.v", line 574, characters 40-43:
The command has indeed failed with message:
add is not a constructor of an inductive type.
File "./output/NumberNotations.v", line 578, characters 0-103:
The command has indeed failed with message:
Missing mapping for constructor Iempty.
File "./output/NumberNotations.v", line 592, characters 56-61:
Warning: Type of I'sum seems incompatible with the type of sum.
Expected type is: (I' -> I' -> I') instead of (I -> I' -> I').
This might yield ill typed terms when using the notation.
[via-type-mismatch,numbers,default]
File "./output/NumberNotations.v", line 597, characters 32-33:
Warning: I was already mapped to Set, mapping it also to
nat might yield ill typed terms when using the notation.
[via-type-remapping,numbers,default]
File "./output/NumberNotations.v", line 597, characters 37-42:
Warning: Type of Iunit seems incompatible with the type of O.
Expected type is: I instead of I.
This might yield ill typed terms when using the notation.
[via-type-mismatch,numbers,default]
File "./output/NumberNotations.v", line 601, characters 0-146:
The command has indeed failed with message:
'via' and 'abstract' cannot be used together.
File "./output/NumberNotations.v", line 680, characters 21-23:
Warning: Type of I1 seems incompatible with the type of Fin.F1.
Expected type is: (nat -> I) instead of I.
This might yield ill typed terms when using the notation.
[via-type-mismatch,numbers,default]
File "./output/NumberNotations.v", line 680, characters 35-37:
Warning: Type of IS seems incompatible with the type of Fin.FS.
Expected type is: (nat -> I -> I) instead of (I -> I).
This might yield ill typed terms when using the notation.
[via-type-mismatch,numbers,default]
File "./output/NumberNotations.v", line 683, characters 11-12:
The command has indeed failed with message:
The term "0" has type "forall n : nat, Fin.t (S n)"
while it is expected to have type "nat".
0
     : Fin.t (S ?n)
where
?n : [ |- nat]
1
     : Fin.t (S (S ?n))
where
?n : [ |- nat]
2
     : Fin.t (S (S (S ?n)))
where
?n : [ |- nat]
3
     : Fin.t (S (S (S (S ?n))))
where
?n : [ |- nat]
0 : Fin.t 3
     : Fin.t 3
1 : Fin.t 3
     : Fin.t 3
2 : Fin.t 3
     : Fin.t 3
File "./output/NumberNotations.v", line 696, characters 11-42:
The command has indeed failed with message:
The term "3" has type "Fin.t (S (S (S (S ?n))))"
while it is expected to have type "Fin.t 3".
@Fin.F1 ?n
     : Fin.t (S ?n)
where
?n : [ |- nat]
@Fin.FS (S ?n) (@Fin.F1 ?n)
     : Fin.t (S (S ?n))
where
?n : [ |- nat]
@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n))
     : Fin.t (S (S (S ?n)))
where
?n : [ |- nat]
@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))
     : Fin.t (S (S (S (S ?n))))
where
?n : [ |- nat]
@Fin.F1 (S (S O)) : Fin.t (S (S (S O)))
     : Fin.t (S (S (S O)))
@Fin.FS (S (S O)) (@Fin.F1 (S O)) : Fin.t (S (S (S O)))
     : Fin.t (S (S (S O)))
@Fin.FS (S (S O)) (@Fin.FS (S O) (@Fin.F1 O)) : Fin.t (S (S (S O)))
     : Fin.t (S (S (S O)))
File "./output/NumberNotations.v", line 705, characters 11-12:
The command has indeed failed with message:
The term
 "@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))"
has type "Fin.t (S (S (S (S ?n))))" while it is expected to have type
 "Fin.t (S (S (S O)))".
0
     : list unit
1
     : list unit
2
     : list unit
2
     : list unit
0 :: 0 :: nil
     : list nat
0
     : Ip nat bool
1
     : Ip nat bool
2
     : Ip nat bool
3
     : Ip nat bool
1
     : Ip nat bool
1
     : Ip nat bool
1
     : Ip nat bool
1
     : Ip nat bool
Ip0 nat nat 1
     : Ip nat nat
Ip0 bool bool 1
     : Ip bool bool
Ip1 nat nat 1
     : Ip nat nat
Ip3 1 nat nat
     : Ip nat nat
Ip0 nat bool O
     : Ip nat bool
Ip1 bool nat (S O)
     : Ip nat bool
Ip2 nat (S (S O)) bool
     : Ip nat bool
Ip3 (S (S (S O))) nat bool
     : Ip nat bool
0
     : 0 = 0
eq_refl
     : 1 = 1
0
     : 0 = 0
eq_refl
     : id 0 = id 0
eq_refl
     : 1 = 1
0
     : 0 = 0
eq_refl
     : id 0 = id 0
2
     : extra_list_unit
cons O unit tt (cons O unit tt (nil O unit))
     : extra_list unit
0
     : Set
1
     : Set
2
     : Set
3
     : Set
Empty_set
     : Set
unit
     : Set
sum unit unit
     : Set
sum unit (sum unit unit)
     : Set
0
     : Fin.t (S ?n)
where
?n : [ |- nat]
1
     : Fin.t (S (S ?n))
where
?n : [ |- nat]
2
     : Fin.t (S (S (S ?n)))
where
?n : [ |- nat]
3
     : Fin.t (S (S (S (S ?n))))
where
?n : [ |- nat]
0 : Fin.t 3
     : Fin.t 3
1 : Fin.t 3
     : Fin.t 3
2 : Fin.t 3
     : Fin.t 3
File "./output/NumberNotations.v", line 933, characters 11-42:
The command has indeed failed with message:
The term "3" has type "Fin.t (S (S (S (S ?n))))"
while it is expected to have type "Fin.t 3".
@Fin.F1 ?n
     : Fin.t (S ?n)
where
?n : [ |- nat]
@Fin.FS (S ?n) (@Fin.F1 ?n)
     : Fin.t (S (S ?n))
where
?n : [ |- nat]
@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n))
     : Fin.t (S (S (S ?n)))
where
?n : [ |- nat]
@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))
     : Fin.t (S (S (S (S ?n))))
where
?n : [ |- nat]
@Fin.F1 (S (S O)) : Fin.t (S (S (S O)))
     : Fin.t (S (S (S O)))
@Fin.FS (S (S O)) (@Fin.F1 (S O)) : Fin.t (S (S (S O)))
     : Fin.t (S (S (S O)))
@Fin.FS (S (S O)) (@Fin.FS (S O) (@Fin.F1 O)) : Fin.t (S (S (S O)))
     : Fin.t (S (S (S O)))
File "./output/NumberNotations.v", line 942, characters 11-12:
The command has indeed failed with message:
The term
 "@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))"
has type "Fin.t (S (S (S (S ?n))))" while it is expected to have type
 "Fin.t (S (S (S O)))".
0
     : Fin.t (S ?n)
where
?n : [ |- nat : Set]
1
     : Fin.t (S (S ?n))
where
?n : [ |- nat : Set]
2
     : Fin.t (S (S (S ?n)))
where
?n : [ |- nat : Set]
3
     : Fin.t (S (S (S (S ?n))))
where
?n : [ |- nat : Set]
0 : Fin.t 3
     : Fin.t 3
1 : Fin.t 3
     : Fin.t 3
2 : Fin.t 3
     : Fin.t 3
File "./output/NumberNotations.v", line 987, characters 11-42:
The command has indeed failed with message:
The term "3" has type "Fin.t (S (S (S (S ?n))))"
while it is expected to have type "Fin.t 3".
@Fin.F1 ?n
     : Fin.t (S ?n)
where
?n : [ |- nat : Set]
@Fin.FS (S ?n) (@Fin.F1 ?n)
     : Fin.t (S (S ?n))
where
?n : [ |- nat : Set]
@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n))
     : Fin.t (S (S (S ?n)))
where
?n : [ |- nat : Set]
@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))
     : Fin.t (S (S (S (S ?n))))
where
?n : [ |- nat : Set]
@Fin.F1 (S (S O)) : Fin.t (S (S (S O)))
     : Fin.t (S (S (S O)))
@Fin.FS (S (S O)) (@Fin.F1 (S O)) : Fin.t (S (S (S O)))
     : Fin.t (S (S (S O)))
@Fin.FS (S (S O)) (@Fin.FS (S O) (@Fin.F1 O)) : Fin.t (S (S (S O)))
     : Fin.t (S (S (S O)))
File "./output/NumberNotations.v", line 996, characters 11-12:
The command has indeed failed with message:
The term
 "@Fin.FS (S (S (S ?n))) (@Fin.FS (S (S ?n)) (@Fin.FS (S ?n) (@Fin.F1 ?n)))"
has type "Fin.t (S (S (S (S ?n))))" while it is expected to have type
 "Fin.t (S (S (S O)))".
0%float
     : float
1%float
     : float
infinity
     : float
neg_infinity
     : float
nan
     : float
2
     : nunit2
2
     : nunit2
NUnit 3
     : nunit 3
NUnit 0
     : nunit 0
NUnit (1 + 1)
     : nunit (1 + 1)