Quelle Arguments_renaming.out
Sprache: unbekannt
|
|
Untersuchungsergebnis.out Download desUnknown {[0] [0] [0]}zum Wurzelverzeichnis wechseln
File "./output/Arguments_renaming.v", line 2, characters 0-36:
The command has indeed failed with message:
Flag "rename" expected to rename A into B.
File "./output/Arguments_renaming.v", line 3, characters 0-19:
Warning: This command is just asserting the names of arguments of eq. If this
is what you want, add ': assert' to silence the warning. If you want to clear
implicit arguments, add ': clear implicits'. If you want to clear notation
scopes, add ': clear scopes' [arguments-assert,vernacular,default]
@eq_refl
: forall (B : Type) (y : B), y = y
eq_refl
: ?y = ?y
where
?y : [ |- nat]
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x.
Arguments eq {A}%_type_scope x _
Arguments eq_refl {B}%_type_scope {y}, [_] _
(where some original arguments have been renamed)
eq_refl : forall {B : Type} {y : B}, y = y
eq_refl is template universe polymorphic
Arguments eq_refl {B}%_type_scope {y}, [_] _
(where some original arguments have been renamed)
Expands to: Constructor Corelib.Init.Logic.eq_refl
Declared in library Corelib.Init.Logic, line 379, characters 4-11
Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x.
Arguments myEq B%_type_scope x _
Arguments myrefl {C}%_type_scope x _
(where some original arguments have been renamed)
myrefl : forall {C : Type} (x : A), C -> myEq C x x
myrefl is template universe polymorphic
Arguments myrefl {C}%_type_scope x _
(where some original arguments have been renamed)
myrefl uses section variable A.
Expands to: Constructor Arguments_renaming.Test1.myrefl
Declared in library Arguments_renaming, line 25, characters 40-46
myplus =
fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S n' => S (myplus T t n' m)
end
: forall {T : Type}, T -> nat -> nat -> nat
Arguments myplus {Z}%_type_scope !t (!n m)%_nat_scope
(where some original arguments have been renamed)
myplus : forall {Z : Type}, Z -> nat -> nat -> nat
myplus is not universe polymorphic
Arguments myplus {Z}%_type_scope !t (!n m)%_nat_scope
(where some original arguments have been renamed)
The reduction tactics unfold myplus when the 2nd and
3rd arguments evaluate to a constructor
myplus is transparent
Expands to: Constant Arguments_renaming.Test1.myplus
Declared in library Arguments_renaming, line 31, characters 9-15
@myplus
: forall Z : Type, Z -> nat -> nat -> nat
Inductive myEq (A B : Type) (x : A) : A -> Prop :=
myrefl : B -> myEq A B x x.
Arguments myEq (A B)%_type_scope x _
Arguments myrefl A%_type_scope {C}%_type_scope x _
(where some original arguments have been renamed)
myrefl : forall (A : Type) {C : Type} (x : A), C -> myEq A C x x
myrefl is template universe polymorphic
Arguments myrefl A%_type_scope {C}%_type_scope x _
(where some original arguments have been renamed)
Expands to: Constructor Arguments_renaming.myrefl
Declared in library Arguments_renaming, line 25, characters 40-46
myrefl
: forall (A C : Type) (x : A), C -> myEq A C x x
myplus =
fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S n' => S (myplus T t n' m)
end
: forall {T : Type}, T -> nat -> nat -> nat
Arguments myplus {Z}%_type_scope !t (!n m)%_nat_scope
(where some original arguments have been renamed)
myplus : forall {Z : Type}, Z -> nat -> nat -> nat
myplus is not universe polymorphic
Arguments myplus {Z}%_type_scope !t (!n m)%_nat_scope
(where some original arguments have been renamed)
The reduction tactics unfold myplus when the 2nd and
3rd arguments evaluate to a constructor
myplus is transparent
Expands to: Constant Arguments_renaming.myplus
Declared in library Arguments_renaming, line 31, characters 9-15
@myplus
: forall Z : Type, Z -> nat -> nat -> nat
File "./output/Arguments_renaming.v", line 49, characters 0-36:
The command has indeed failed with message:
Argument lists should agree on the names they provide.
File "./output/Arguments_renaming.v", line 50, characters 0-41:
The command has indeed failed with message:
Sequences of implicit arguments must be of different lengths.
File "./output/Arguments_renaming.v", line 51, characters 0-37:
The command has indeed failed with message:
Argument number 3 is a trailing implicit, so it can't be declared non
maximal. Please use { } instead of [ ].
File "./output/Arguments_renaming.v", line 52, characters 0-37:
The command has indeed failed with message:
Argument z is a trailing implicit, so it can't be declared non maximal.
Please use { } instead of [ ].
File "./output/Arguments_renaming.v", line 53, characters 0-28:
The command has indeed failed with message:
Extra arguments: y.
File "./output/Arguments_renaming.v", line 54, characters 0-26:
The command has indeed failed with message:
Flag "rename" expected to rename A into R.
File "./output/Arguments_renaming.v", line 58, characters 2-36:
The command has indeed failed with message:
Arguments of section variables such as allTrue may not be renamed.
[ zur Elbe Produktseite wechseln0.90Quellennavigators
]
|
2026-03-28
|
