Quelle example1.v Sprache: Coq

Require Import Ltac2.Ltac2.

Import Ltac2.Control.

(** Alternative implementation of the hyp primitive *)
Ltac2 get_hyp_by_name x :=
  let h := hyps () in
  let rec find x l := match l with
  | [] => zero Not_found
  | p :: l =>
    match p with
    | (id, _, t) =>
      match Ident.equal x id with
      | true => t
      | false => find x l
      end
    end
  end in
  find x h.

Print Ltac2 get_hyp_by_name.

Goal forall n m, n + m = 0 -> n = 0.
Proof.
refine (fun () => '(fun n m H => _)).
let t := get_hyp_by_name @H in Message.print (Message.of_constr t).
Abort.

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

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.