Quelle ltac.v Sprache: Coq

Set Ltac Backtrace.

(* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *)
Goal True.
Fail let T := constr:((fun a b : nat => a+b) 1 1) in
  lazymatch T with
  | (fun x z => ?y) 1 1
    => pose ((fun x _ => y) 1 1)
  end.
Abort.

(* This should not raise a warning (see #4317) *)
Goal True.
assert (H:= eq_refl ((fun x => x) 1)).
let HT := type of H in
lazymatch goal with
| H1 : HT |- _ => idtac
end.
Abort.

Ltac f x y z :=
  symmetry in x, y;
  auto with z;
  auto;
  intros;
  clearbody x;
  generalize dependent z.

Print Ltac f.

(* Error messages *)

Ltac g1 x := refine x.
Tactic Notation "g2" constr(x) := g1 x.
Tactic Notation "f1" constr(x) := refine x.
Ltac f2 x := f1 x.
Goal False.
Fail g1 I.
Fail f1 I.
Fail g2 I.
Fail f2 I.
Abort.

Ltac h x := injection x.
Goal True -> False.
Fail h I.
intro H.
Fail h H.
Abort.

(* Check printing of the "var" argument "Hx" *)
Ltac m H := idtac H; exact H.
Goal True.
let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac.
Abort.

(* Check consistency of interpretation scopes (#4398) *)

Goal nat*(0*0=0) -> nat*(0*0=0). intro.
match goal with H: ?x*?y |- _ => idtac x end.
match goal with |- ?x*?y => idtac x end.
match goal with H: context [?x*?y] |- _ => idtac x end.
match goal with |- context [?x*?y] => idtac x end.
Abort.

(* Check printing of let in Ltac and Tactic Notation *)

Ltac foo :=
  let x := intros in
  let y := intros -> in
  let v := constr:(@ nil True) in
  let w := () in
  let z := 1 in
  pose v.
Print Ltac foo.

(* Ltac renaming was not applied to "fix" and "cofix" *)

Goal forall a, a = 0.
match goal with
|- (forall x, x = _) => assert (forall n, (fix x n := match n with O => O | S n => x n end) n = n)
end.
intro.
Show.
Abort.

quality100%

¤ Dauer der Verarbeitung: 0.4 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.