Quelle ltac1_conversions.v Sprache: Coq

Require Import Ltac2.Ltac2.

Ltac2 Type exn ::= [ Got (Std.intro_pattern option) ].

(* we can't return a value from a ltac1 notation so we get it out using Control.zero *)
Tactic Notation "foo" simple_intropattern(x) :=
  let f := ltac2:(y |- Control.zero (Got (Ltac1.to_intro_pattern y))) in
  f x.

Ltac2 Notation "ipat" x(intropattern) := x.

Goal nat. (* we need an open goal because ltac1 auto focuses *)
  Ltac2 Eval match Control.case (fun () => ltac1:(foo y%nat)) with
    | Err (Got (Some (Std.IntroAction
                         (Std.IntroApplyOn
                            c
                            (Std.IntroNaming (Std.IntroIdentifier id)))))) =>
        Control.assert_true (Ident.equal id @y);
        match! c () with
        | nat => ()
        | _ => Control.throw Assertion_failure
        end
    | Val _ | Err _ => Control.throw Assertion_failure
    end.

  Ltac2 Eval match Ltac1.to_intro_pattern (Ltac1.of_intro_pattern (ipat ?w)) with
    | Some (Std.IntroNaming (Std.IntroFresh id)) => Control.assert_true (Ident.equal id @w)
    | _ => Control.throw Assertion_failure
    end.

  Ltac2 Eval
    ltac1:(
      let n := numgoals in
      let t := ltac2:(n |-
        match Ltac1.to_int n with
        | Some 1 => ()
        | _ => Control.throw Assertion_failure
        end)
      in
      t n).

  Fail Ltac2 Eval
    ltac1:(
      let n := numgoals in
      let t := ltac2:(n |-
        match Ltac1.to_int n with
        | None => ()
        | _ => Control.throw Assertion_failure
        end)
      in
      t n).

  Ltac2 Eval
   ltac1:(n |- do n assert False; [| | |]) (Ltac1.of_int 2).

Abort.

quality95%

¤ 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.