| products/sources/formale Sprachen/Coq/test-suite/output/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: List_Cpo.thy Sprache: Unknown
|
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.85Quellennavigators ] |