Quellcode-Bibliothek quot.v Sprache: Coq

Require Import Ltac2.Ltac2.

(** Test for quotations *)

Ltac2 ref0 () := reference:(&x).
Ltac2 ref1 () := reference:(nat).
Ltac2 ref2 () := reference:(Datatypes.nat).
Fail Ltac2 ref () := reference:(i_certainly_dont_exist).
Fail Ltac2 ref () := reference:(And.Me.neither).

Goal True.
Proof.
let x := constr:(I) in
let y := constr:((fun z => z) $x) in
Control.refine (fun _ => y).
Qed.

Goal True.
Proof.
(** Here, Ltac2 should not put its variables in the same environment as
Ltac1 otherwise the second binding fails as x is bound but not an
ident. *)
let x := constr:(I) in
let y := constr:((fun x => x) $x) in
Control.refine (fun _ => y).
Qed.

quality94%

¤ 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.0.7Bemerkung: ¤

*Bot Zugriff

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.