Quelle bug_11677.v Sprache: Coq

Require Import Ltac2.Init.
Require Ltac2.Control.
Require Ltac2.Ltac1.

Ltac2 drop_first_success (tac : unit -> 'a) :=
  match Control.case tac with
  | Val v
    => let (first_success, next) := v in
       fun (v : unit) => next (Tactic_failure None)
  | Err err => Control.zero err
  end.

Ltac drop_first_success tac :=
  let f := ltac2:(tac1 |- drop_first_success (fun () => Ltac1.run tac1) ()) in
  f tac.

Ltac drop_n_success n tac :=
  lazymatch n with
  | O => tac
  | S ?n => drop_n_success n ltac:(drop_first_success tac)
  end.

Ltac only_nth_success n tac :=
  once (drop_n_success n tac).

Set Default Proof Mode "Classic".

Goal True \/ False.
  drop_first_success ltac:(idtac "a"; constructor).
(* Error: Uncaught Ltac2 exception: Tactic_failure (None) *)
Abort.

quality100%

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