Quelle NumberNotations.out
Sprache: unbekannt
|
|
Untersuchungsergebnis.out Download desUnknown {[0] [0] [0]}zum Wurzelverzeichnis wechseln
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)
[ zur Elbe Produktseite wechseln0.112Quellennavigators
]
|
2026-03-28
|
