Untersuchungsergebnis.out Download desScala {Scala[46] Latech[108] CS[110]}zum Wurzelverzeichnis wechseln
3 focused subgoals
(shelved: 1)
============================
?Goal 0
subgoal 2 is:
forall n : nat, ?Goal n -> ?Goal (S n)
subgoal 3 is:
nat
unification constraint:
?Goal ?Goal2 <=
True /\ True /\ True \/
veeryyyyyyyyyyyyloooooooooooooonggidentifier =
veeryyyyyyyyyyyyloooooooooooooonggidentifier
3 focused subgoals
(shelved: 1)
n, m : nat
============================
?Goal@{n:=n; m:=m} 0
subgoal 2 is:
forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0)
subgoal 3 is:
nat
unification constraint:
?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <=
True /\ True /\ True \/
veeryyyyyyyyyyyyloooooooooooooonggidentifier =
veeryyyyyyyyyyyyloooooooooooooonggidentifier
3 focused subgoals
(shelved: 1)
m : nat
============================
?Goal1@{m:=m} 0
subgoal 2 is:
forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0)
subgoal 3 is:
nat
unification constraint:
n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <=
True /\ True /\ True \/
veeryyyyyyyyyyyyloooooooooooooonggidentifier =
veeryyyyyyyyyyyyloooooooooooooonggidentifier
3 focused subgoals
(shelved: 1)
m : nat
============================
?Goal0@{m:=m} 0
subgoal 2 is:
forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0)
subgoal 3 is:
nat
unification constraint:
n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <=
True /\ True /\ True \/
veeryyyyyyyyyyyyloooooooooooooonggidentifier =
veeryyyyyyyyyyyyloooooooooooooonggidentifier
The command has indeed failed with message:
In environment
P : nat -> Type
x : nat
h : P x
Unable to unify "P x" with "?P x"
(unable to find a well-typed instantiation for "?P": cannot ensure that
"nat -> Type" is a subtype of "nat -> Prop").
[ zur Elbe Produktseite wechseln0.99Quellennavigators
]
