Columbo aufrufen.out zum Wurzelverzeichnis wechselnHaskell {Haskell[224] CS[430] Ada[447]}Datei anzeigen
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
[ Original von:0.808Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen.
Man kann per Verzeichnistruktur darin navigieren.
Der Code wird farblich markiert angezeigt.
]
