Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
RPCMemoryParams.thy
Sprache: Isabelle
Untersuchungsergebnis.out Download desHaskell {Haskell[237] CS[481] Ada[492]}zum Wurzelverzeichnis wechseln
The command has indeed failed with message:
Flag "rename" expected to rename A into B.
File "stdin", line 3, characters 0-25:
Warning: This command is just asserting the names of arguments of identity.
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]
@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
For eq_refl: Arguments are renamed to B, y
For eq: Argument A is implicit and maximally inserted
For eq_refl, when applied to no arguments:
Arguments B, y are implicit and maximally inserted
For eq_refl, when applied to 1 argument:
Argument B is implicit
For eq: Argument scopes are [type_scope _ _]
For eq_refl: Argument scopes are [type_scope _]
eq_refl : forall (A : Type) (x : A), x = x
eq_refl is not universe polymorphic
Arguments are renamed to B, y
When applied to no arguments:
Arguments B, y are implicit and maximally inserted
When applied to 1 argument:
Argument B is implicit
Argument scopes are [type_scope _]
Expands to: Constructor Coq.Init.Logic.eq_refl
Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x
For myrefl: Arguments are renamed to C, x, _
For myrefl: Argument C is implicit and maximally inserted
For myEq: Argument scopes are [type_scope _ _]
For myrefl: Argument scopes are [type_scope _ _]
myrefl : forall (B : Type) (x : A), B -> myEq B x x
myrefl is not universe polymorphic
Arguments are renamed to C, x, _
Argument C is implicit and maximally inserted
Argument scopes are [type_scope _ _]
Expands to: Constructor Arguments_renaming.Test1.myrefl
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 are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
myplus : forall T : Type, T -> nat -> nat -> nat
myplus is not universe polymorphic
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
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
@myplus
: forall Z : Type, Z -> nat -> nat -> nat
Inductive myEq (A B : Type) (x : A) : A -> Prop :=
myrefl : B -> myEq A B x x
For myrefl: Arguments are renamed to A, C, x, _
For myrefl: Argument C is implicit and maximally inserted
For myEq: Argument scopes are [type_scope type_scope _ _]
For myrefl: Argument scopes are [type_scope type_scope _ _]
myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
myrefl is not universe polymorphic
Arguments are renamed to A, C, x, _
Argument C is implicit and maximally inserted
Argument scopes are [type_scope type_scope _ _]
Expands to: Constructor Arguments_renaming.myrefl
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 are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
myplus : forall T : Type, T -> nat -> nat -> nat
myplus is not universe polymorphic
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
The reduction tactics unfold myplus when the 2nd and
3rd arguments evaluate to a constructor
myplus is transparent
Expands to: Constant Arguments_renaming.myplus
@myplus
: forall Z : Type, Z -> nat -> nat -> nat
The command has indeed failed with message:
Argument lists should agree on the names they provide.
The command has indeed failed with message:
Sequences of implicit arguments must be of different lengths.
The command has indeed failed with message:
Some argument names are duplicated: F
The command has indeed failed with message:
Argument number 2 (anonymous in original definition) cannot be declared
implicit.
The command has indeed failed with message:
Extra arguments: y.
The command has indeed failed with message:
Flag "rename" expected to rename A into R.
[ zur Elbe Produktseite wechseln0.117Quellennavigators
]
|
|
