| products/sources/formale sprachen/Coq/test-suite/output/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: Search.v Sprache: Coq
|
Untersuchungsergebnis.out Download desHaskell {Haskell[224] CS[430] Ada[447]}zum Wurzelverzeichnis wechseln The command has indeed failed with message: Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := symmetry in x, y; auto with z; auto; intros; clearbody x; generalize dependent z The command has indeed failed with message: In nested Ltac calls to "g1" and "refine (uconstr)", last call failed. The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: In nested Ltac calls to "f1 (constr)" and "refine (uconstr)", last call failed. The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: In nested Ltac calls to "g2 (constr)", "g1" and "refine (uconstr)", last call failed. The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: In nested Ltac calls to "f2", "f1 (constr)" and "refine (uconstr)", last call failed. The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. No primitive equality found. The command has indeed failed with message: In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. No primitive equality found. Hx nat nat 0 0 Ltac foo := let x := intros in let y := intros -> in let v := constr:(nil) in let w := () in let z := 1 in pose v 2 subgoals n : nat ============================ (fix a (n0 : nat) : nat := match n0 with | 0 => 0 | S n1 => a n1 end) n = n subgoal 2 is: forall a : nat, a = 0 [ zur Elbe Produktseite wechseln0.140Quellennavigators ] |