|
(* Check that the presence of binders with type annotation do not
prevent the recursive binder part to be found *)
From Coq Require Import Utf8.
Delimit Scope C_scope with C.
Global Open Scope C_scope.
Delimit Scope uPred_scope with I.
Definition FORALL {T : Type} (f : T → Prop) : Prop := ∀ x, f x.
Notation "∀ x .. y , P" :=
(FORALL (λ x, .. (FORALL (λ y, P)) ..)%I)
(at level 200, x binder, y binder, right associativity) : uPred_scope.
Infix "∧" := and : uPred_scope.
(* The next command fails with
In recursive notation with binders, Φ is expected to come without type.
I would expect this notation to work fine, since the ∀ does support
type annotation.
*)
Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
(∀ Φ : _ → _,
(∀ x, .. (∀ y, Q ∧ Φ pat) .. ))%I
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e {{{ x .. y ; pat , Q } } }") : uPred_scope.
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
