Quelle Tactics.v Sprache: Coq

(* Test printing of Tactic Notation *)

Tactic Notation "a" constr(x) := apply x.
Tactic Notation "e" constr(x) := exact x.

Ltac f H := split; [a H|e H].
Print Ltac f.

(* Test printing of match context *)
(* Used to fail after translator removal (see BZ#1070) *)

Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end.
Print Ltac g.

(* Test an error message (BZ#5390) *)
Lemma myid (P : Prop) : P <-> P.
Proof. split; auto. Qed.

Goal True -> (True /\ True) -> True.
Proof.
intros H.
Fail intros [H%myid ?].
Fail destruct 1 as [H%myid ?].
Abort.

(* Test that assert_succeeds only runs a tactic once *)
Ltac should_not_loop := idtac + should_not_loop.
Goal True.
  assert_succeeds should_not_loop.
  assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *)
Abort.

(* assert_succeeds preserves the error *)
Goal True.
  Fail assert_succeeds exact False.
Abort.

Module IntroWildcard.

Theorem foo : { p:nat*nat & p = (0,0) } -> True.
Fail intros ((n,_),H).
Abort.

End IntroWildcard.

Module ApplyIn.

Ltac test a b c d e := apply a, b in c as [], d, e as ->.
Print test.

End ApplyIn.

quality100%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.