From 055b44323a770cd45206f0670463b03df2e3b386 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 17 Jun 2014 23:35:03 +0200
Subject: [PATCH] Extend the frontend language with break/continue, named
variables, and static variables.
---
theories/base.v | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/theories/base.v b/theories/base.v
index cf7f74c5..a9c3cfdd 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -407,15 +407,18 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.
Notation "x ← y ; z" := (y ≫= (λ x : _, z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
-Notation "'( x1 , x2 ) ← y ; z" :=
+Notation "' ( x1 , x2 ) ← y ; z" :=
(y ≫= (λ x : _, let ' (x1, x2) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
-Notation "'( x1 , x2 , x3 ) ← y ; z" :=
+Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
(y ≫= (λ x : _, let ' (x1,x2,x3) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
-Notation "'( x1 , x2 , x3 , x4 ) ← y ; z" :=
+Notation "' ( x1 , x2 , x3 , x4 ) ← y ; z" :=
(y ≫= (λ x : _, let ' (x1,x2,x3,x4) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
+Notation "' ( x1 , x2 , x3 , x4 , x5 ) ← y ; z" :=
+ (y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
+ (at level 65, next at level 35, only parsing, right associativity) : C_scope.
Class MGuard (M : Type → Type) :=
mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
--
GitLab