The command has indeed failed with message:
Unexpected term (nat -> nat) while parsing a number notation.
The command has indeed failed with message:
Unexpected non-option term opaque4 while parsing a number notation.
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
The command has indeed failed with message:
Cannot interpret this number as a value of type unit
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 "stdin", 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]
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}".
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
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
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 "stdin", 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]
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]
let v := of_uint (Number.UIntDecimal (Decimal.D1 Decimal.Nil)) in v : unit
     : unit
let v := 0%test13 in v : unit
     : unit
The command has indeed failed with message:
to_uint' is bound to a notation that does not denote a reference.
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".
The command has indeed failed with message:
to_uint'' is bound to a notation that does not denote a reference.
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
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".
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".
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
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
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".
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".
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
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
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)%Z
     : Z
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
The command has indeed failed with message:
Missing mapping for constructor Isum.
The command has indeed failed with message:
Iunit was already mapped to unit and cannot be remapped to unit.
The command has indeed failed with message:
add is not an inductive type.
The command has indeed failed with message:
add is not a constructor of an inductive type.
The command has indeed failed with message:
Missing mapping for constructor Iempty.
File "stdin", line 577, 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]
File "stdin", line 582, 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]
File "stdin", line 582, 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]
The command has indeed failed with message:
'via' and 'abstract' cannot be used together.
File "stdin", line 662, 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]
File "stdin", line 662, 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]
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
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)))
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
     : 1 = 1
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
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)))
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
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)))
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)))".