Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Curly braces in Coq notations

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Curly braces in Coq notations


Chronological Thread 
  • From: Benjamin Pierce <bcpierce AT cis.upenn.edu>
  • To: Benjamin Pierce <bcpierce AT cis.upenn.edu>, coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Curly braces in Coq notations
  • Date: Mon, 23 Oct 2023 09:29:09 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mail-vs1-f45.google.com
  • Ironport-data: A9a23:JgoGP6lv4hhNiKYzHB2PO/zo5gwWIkRdPkR7XQ2eYbSJt1+Wr1Gzt xIZXmyDOq6Oajb1L4xxYYW/808H7MTQyYVqT1Bvry5gRVtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayajl8B56r8ks1562q4mhA5zTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1/AhEJH6cy/t9mJkZPq /0lAmkiZBW60rfeLLKTEoGAh+wmJcjveZ0E4zRukWyfAvEhTpTOBa7N4Le03h9q3pEITauYP ZNGL2YyBPjDS0Un1lM/ApkmneqyjXTXaDBRsxSIvacx5S7ewBEZPL3FbouIIoLWHZg9ckCwi jr9/UPyLjgmafuwzzid9WO3is6WpHauMG4VPOTgqqQCbEeo7mcUEVgdUUaxieKoj1a3HdNZM U0dvCQ0xZXe72SuR9j5GgOj+TuK4kNaVN1XHOk3rgqKz8I4/jp1GEAVQG5+SvYMsPYnYhsri F60tYrGDzlW5ej9pW2myp+Yqja7OC4wJGAEZDMZQQZt3zUFiNFj5v4oZoYzeJNZnuEZChmrn G/X9HlWa6E7yJ9Uh//irDgrlhr1/sCRJjPZ8Dk7SY5M0++UTIusZojt90OCqPgcccCWSV6Ou HVCkM+bhAzvMX1vvH3XKAnuNOvxjxpgDNE6qQM/d3XG32r1k0NPhagKvFlDyL5Ba67ogwPBb k7Joh9275ROJnasZqIfS9vvWpt7nPm8Toq1B6i8gj9yjn5ZJF/vEMZGNR744owRuBVEfVwXY MjKLZvzXR7294w9lmrpHo/xLoPHNghnnT+JLXwK5xug1rWaaRaopUQtYTOzghQCxPrc+m39q o4BX+PTkkk3eLOkPkH/r9VIRXhUdihTOHwDg5YIHgJ1ClE2Rj9J5j646e9JRrGJaIwPxruTp yHjBRADoLc97FWeQTi3hrlYQOuHdf5CQbgTZETA5H75iiBxUpXl96oFaZo8cJ8u8eEpn7Y+T OAId4/ESr5DQyjOsWZVJ5Tsjp1QRDLyjyK3Pg2hfGceebxkTFf34dPKRFbk2xQPKSuVjvEAh YOc+DnVerc5fDQ6Pv3qMKqu63iToUkinPlDWhqUA9tLJ2Tp3otYCw3wqf4VIcg8DAjP9hGe3 QPKHCUnn7DsopA0wvbNl6urv4ekKMogP0t4Tk3wz6e6CjnexUWnmbR/aeeveSvMcl/09IGJR /Rn/9ulPNIpxF914pdBSZB1xqcA1v7Tjr59zDU8Ok7Ubl6uW4hSElPf0eZh7qRyl6Jk4y2oU Uey+/5fC7WDGOXhNHUzfAMFTOCy5cs4qwnoz8YeARvFvXds3b+9T09tEQGGi3VdIJtLIYoV+ 7odl/BM2TOvqCgBE4igtT9VxVSuP3ZbcqQAt7MmOqHJpDcv6Gl/Zc37NnerzrCJM85BI2s7E A+y3aDivYlR9mDGUng0FEXO49ZjuIQziEh062EGdnu0mYvjp/4o3Rdu3yw9YSZLwz5mje9iG GhZGHdkBKeJ/jwyushITj31EC5/GReYp0jD62YIsEb7TECYcHPHA0NgGOSK/WEfq3l9eBoC9 p6m6W/VaxTYV+Cv4TkXRmhetO3Fcdx90ibgifKXNZ2JMLdiaAW0n5L0Q3QDriXWJP8YhWrFl LFMx/lxY6iqDhwgifQ3JKfC3ItBVS3eAnJJRMxg26Y7HWv8XjWW8hrWImCTfvJ9HdD7wXWaO edPeP0WDw+f0RyQpA81HaQPer94vMA47eo4J4/EGzQ0jKu9nBFI7rTr6SnMtE06SY5PkOE8C L/rWRCsL2iyvUZQykjx9JRqG2zgetQVRhzO7Mbs+sUzKp8zmuVNc0Yz77iKg0uoIDZXpxK6g C6TZov97fBT9oB3ro69ToRBH1qVLP3wZsSp8Seykch/UtfUFff8pSYu81zBEzlLD+FAReYth bCptfjp1njkp5czaXjSwLOaJplK5OKzfetZCd32J39khhm/WNfgzh8A2mKgI7lbuYl5yuj+Y CXgc+q2V9oee+kF9U1vcyIETiosUfXmXJnvtQaWjqqqCCFE9SflMdn+13viTV8DRx8yI5ekV zPF4ae/1Ot58rZJKgQPXcx9IplCJ1TmZ6sqWvvxuRScDUiqmlmygaTjpzVx9QD0DmS4L+ii7 aLnXhTecDGAiJPMxvxdsK1wuUQzJ1R5iu8SYEkc2oBXjxaXMW04FtkeYK42Usxsri/P1Z/GP WCHKCNoDCjmRj1LfCnt+NmpDE/VGuUKPcy/PTAzuV+dbyCtHo6bHb997WFa7mxrfif4hvSSQ T3EFqYc4jDqqn2oeQoS2hB/qeJux/ef2GlRvE6hzor9BBERBbhM33tkdOaIueorDOmV/Hgn5 0BsLYyHfK1/YVX8GN0mZmZYHhdfsT/yp9ntRTna287R4u1308UZoMAS+IjPPnkrZ8URYqMWS HXxAWaB/gh6H5DVVbQB47oUvEO/NR5H8gVW4kMuqc3+UpxcMlgaAv4=
  • Ironport-hdrordr: A9a23:v3cte6xWViObfzX27BIaKrPwFb1zdoMgy1knxilNoH1uA7Wlfq WV9sjzuiWE7Qr5NEtQ++xofZPwIk80lqQV3WByB8bHYOCOggLBR72Kr7GD/9SKIVyYygcy79 YHT0G8MrHN5JpB4PoSLDPWLz/o+re6zJw=
  • Ironport-phdr: A9a23:CG1SURGUqH3fwd66oM4fWp1Gf/RGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k33BmZA86Fs7oE07OQ7/q+HzRYoN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB 89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9sL xi6twbcu8gZjYZjNqo61x/FrmdVd+hMym5kO1Oekwzg6sus+ZJo7jhdte8m+8NcS6vxYr42T aZfDDQoMmA14NPkuBzeRgaR5XUST3sbnANQDwfK8B/1UJHxsjDntuVmwymVIdf2TbEvVju86 apgVQLlhz0GNz4992HXl9BwgadGqx+vuxBz34jZa5yTOfFjfK3SYMkaSHJOUcZfVSNPAo2yY YgSAeQfIelVtJPyq0cUoBakGQWgGOHixzlVjXH2x6061OEhHBnb0QM+GdIOsm7brND0NKcUT Ou71qjIwivZb/xKxzj29Y/FfQs9rvGUXLJ/b9DRxlUxGA7eklqQqJflMymI1uQVrWeb6exgW fixhGE6tgF8uz6izdojhYfVnIwa0EzE9Tlnz4YvI921UE51bN+kHZZRuS+XOIR7T90sTmxmu is31LkLtJqmcCUIxpkpyRrSZfKaf4WL/B/tVPudLCpkiH9lZL6xiQu//VSmx+bhVce0yE5Ho jRZntTIrHwA1Bze5tKZRvdg/EqtwzmC2gDV5+pZO047j7DbJIQkwrMolpocr0DDHijulUXzl qCWd0Ek9vG26+T8f7nqv5GcOoB0hw3kPaQuncu/Aes8MgcQRWSU5eO81Lj78U34RrVFkOE2n 7HHvJzGIckXvK20Dg9P3oo99hqyDS2q3dsYkHUfKVJKYhOHj4znO1HUJ/D4CO+yjE+wnzdzx vDJIKfhDYnTIXXYi7fuY6xy61VGxAou1dBQ+ZRUCrcbLP3tR0DxqcTUDhkiPAOs2eboFM191 p8CWWKIGqKVLbvesUWU6eI3P+mMeIgVtS7hJPgi/v7ilGM2mVsAfaayxpYXc3C5HvF+I0qDe 3bsg9EBEX0LvgUkVuDqhkeCAnZvYCOYUqQ+7zQ6DsqeDIrZTY3l1LaKxCa2BJZbTmtHERaRC XruccOJV+paLGqZJdYkmTgZX5CgTZUg3FegrlzU0b1ie8DZ/C8RsJPlnOB06vfYmFlm/zdsD smH2GylRGBv2H4QSjkwmq1zvBoumR+4zaFkjqkARpRo7PRTX1JiXXa95+lzCtSpHxnEYs/MU 1G+BNOvHTA2SNs1hd4IeUd0Xdu43VjYxyT/JbgTmvSQAYAstLrG1i37LN58xmzN2YEqjkJgX 9NCM2vgi6JipEDIH4Ccq0yCjO6xcLgEmivE9WON122L6UtTSA99S67IdWsSb1CQsMz04EWEQ rOzWvw8KgUU78mEJ+NRb8Hxy1VLQPC2INPFf2e4gHu9Hz6Nz7KIKZTxIiATgHibB08DnAQeu 32BMGDSHw+HpGTTRHxrHFPrOAb39PVm7Wi8Vgkyxh2LaEto0/y0/AQUjLqSUaFb2LVMoyonp zhueTT1l9vLF9qNoRZgd6RAcJs85llAz2fQqw16ONSpMaljglcUdwk/sVnp0l17DYBJkM5iq 31PrkI6I6mA0V5bfD6w1pHrfKDPJ2/0uh2jdu+e213T1sqX5rZa8O4x+DCB9EmiEksv9Wki0 sEAiSPNoMWXSlBLDtStDxVSlVAyvbzRbygj6pmB0HRtNfLxqTrew5cyA/NjzB+8ftBZOafCF QnoEsRcCdL9TY5i01WvcB8AO/hfsaAuOMbzPfGNwK+mJu1ttCmrhH8B/Zhw1ETK+iZhAL2tv d5N07SD0w2LWi2pxl2qqsH6g4tJTToTBSyi0SXiAshcarA4LuNpQS++ZsawwNt5nZvkXXVVo UWiC10x08isYROOblb50GW8zGwvqGe80Wu9xj1wyHQyq7aHmTfJ26LkfQYGPWhCQC9ji03tK M66lYJSUE+tZgkv3ByrgCSyj6JQvKVyNWLeaVxFdjOwMnlvVK32u7afK8JC85IntyxLXf/0O wjLDO6g5UFDjGW/QiNX33gjeiuvu4nlkhAf6irVN3t1oHfDOIlxyRrZ+N3AVKtU1zsCSjN/j GqfDVy9Mt+1uNSMws2b46buCiT7D8IVLXS4qOHI/DG27mBrHxClyvW6m9m8VBM/zTe+zN5yE yPBsBf7ZIDvkaW8K+NuOEdyVzqeo4J3HJ9zlowoidQew38f09+f9mIGnH34PP1A1KvlKmcVS DgNhdPZ/UK2vS8rZmLM3I//WniHl4FrbMG7b3kd1wom4slRTrqM4bpC2yZ5vxDryGCZKeg4l TAbx/w07XcciOxcowshwBKWBbUKFFVZNyjhxFyYqsqzp6JNaCOzYKC9gQBgyMu5AujI8WQ+E D7pP40vFihq4oBjPULQhTftv5r8doCYbMpP5EbJ1U6R164PdM13zr1Q2WJmIT6v4yFjkbVgy 0Uwhdfi+9HWTgcltKOhXkwGaHusP5lVone1yvwG1seOg9LxQNM7RmRNDMOuFbXySHoTrai1a FzISWF68ybBX+KYRF/6ig8urmqTQc/3cSjNeT9Bi40lHUfVJVQD0llMDHNjwcF/Rkbyg5a4O EZhumJIuQW+80oQjLoub16mDAK97E+pcmtmEsDOakoLqFgYtwGNdpXBpuNrQ3MCp8Pn8VzLc z3BIVwPVDBBW1TYVQq6YP/0voiGqLLeXq3nfp6sKf2YoOhaHZ9k3LqJ1Y1rt3aJP8SLZTx5C uEjn1FERTZ/EtjYnDMGT2oWkTjMZoiVvkX0/Co/tc25/PnxPWCnrYKSF7tfN8lu8BGqkO+CM eCXniNwNTdf0NsF23bJzLEV2FNahTtpcnGhFrEJtCiFS6y1+OcfFxkAdyZ6L9dF9Yo51whJf NDA05b7iuM+gfkyBFNIE1fmn4DhZMAHJX28KEKSBEuPM+fjR3WDyMX2bKWgDLxI2b8M5lvg5 HDBShClYmnQ8luhHwqiOuxNkiyBaRlXuYXmNw1oFXCmV9X+LBuyLN5wizQyh7wynHLDc2AGY l0eOwtAqKOd6SRAj7BxAWtEuzBvJvGFljyS4sHDJ58N9+ZzDyJy0e9W/T5prtkdpDEBX/Fzl CbI+5R2pEq6l+CU1jd9eB9HqzIOmpnS+Es+ZOPW8Z5PXXuC9xUIpzb1aVxCt55uDdvhvLpVw 97EmffoKTtMxNnT+NMVG8neLM/v2JUJKhfgA3jJFAYDS3imOXyN3iS1ddmZ92bTs4A3rJ6ql ZYTGOczvL0dE/obDgF7B4VHLssqGDwjlrGfgYgD4n/s9HHs
  • Ironport-sdr: 65367551_PMIMJmX8bHdI5io4pvsuHiL6n21rDMqENnySyFxlAsGZiza 7n3o49RmxtpkP249gt+XT0dstkDq0gMo7rjYHrg==

Thank you!!  

It turns out that 

Notation "{{ f x .. y }}" := (.. (f x) .. y)
                  (in custom com at level 0, only parsing,
                  f constr at level 0, x constr at level 9,
                  y constr at level 9) : com_scope.

(with outer brackets) also works, so I am happy enough with this. 

    - Benjamin

On Mon, Oct 23, 2023 at 7:32 AM Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:
Fixing a typo:
the right-hand side of :=, a term at level 0
-->
the right-hand side of :=, a com at level 85 eventually expected to be a com at level 0

On Mon, Oct 23, 2023 at 01:19:40PM +0200, Hugo Herbelin wrote:
> Hi,
>
> This is also due to the special status of { } which is predefined at
> level 0 with syntax "{ x }". In "(<{ { X > 0 } X := 0 { true } }>)",
> the right-hand side of :=, a term at level 0, is parsed as "0 { true }",
> that is as 0 applied to the notation "{ true }".
>
> I'm afraid you'd have to renounce to the notation
>
> Notation "f x .. y" := (.. (f x) .. y)
>                   (in custom com at level 0, only parsing,
>                   f constr at level 0, x constr at level 9,
>                   y constr at level 9) : com_scope.
>
> in custom entry com, or to replace it e.g. with a notation of the form
> "f ( x , .. , y )", etc.
>
> This special notation "{ x }" was there to implement the "historical"
> notations "{ x } + { y }" for sumbool and "x + { y }" for sumor, and
> their nesting as in "{ x } + { y } + { z }". We did not find a way
> to do it without introducing a stand-alone "{ x }".
>
> Hope it helps,
>
> Hugo
>
> On Sun, Oct 22, 2023 at 04:06:46PM -0400, Benjamin Pierce wrote:
> > Many thanks, Gaëtan!  Yes, this works.
> >
> > May I trouble you (and/or others) with one further question?  When I scale this
> > up to the full Imp language, it seems to get me almost everything I want, but I
> > am still puzzled by why I can't omit the parentheses on the very last line
> > below.  I've tried tweaking various precedence levels, but have not found the
> > right combination...
> >
> >    - B
> >
> >
> >     From Coq Require Import Strings.String. Import String.
> >     From Coq Require Import Bool.Bool.
> >     From Coq Require Import Init.Nat.
> >     From Coq Require Import Arith.Arith.
> >     From Coq Require Import Arith.EqNat. Import Nat.
> >     From Coq Require Import Lia.
> >     From Coq Require Import Lists.List. Import ListNotations.
> >     From PLF Require Import Maps.
> >
> >     Declare Custom Entry com.
> >     Declare Custom Entry com_aux.
> >     Declare Scope com_scope.
> >     Open Scope com_scope.
> >
> >     Definition state := total_map nat.
> >
> >     Inductive aexp : Type :=
> >       | ANum (n : nat)
> >       | AId (x : string)
> >       | APlus (a1 a2 : aexp)
> >       | AMinus (a1 a2 : aexp)
> >       | AMult (a1 a2 : aexp).
> >
> >     Definition W : string := "W".
> >     Definition X : string := "X".
> >     Definition Y : string := "Y".
> >     Definition Z : string := "Z".
> >
> >     Inductive bexp : Type :=
> >       | BTrue
> >       | BFalse
> >       | BEq (a1 a2 : aexp)
> >       | BNeq (a1 a2 : aexp)
> >       | BLe (a1 a2 : aexp)
> >       | BGt (a1 a2 : aexp)
> >       | BNot (b : bexp)
> >       | BAnd (b1 b2 : bexp).
> >
> >     Coercion AId : string >-> aexp.
> >     Coercion ANum : nat >-> aexp.
> >
> >     Notation "<{ e }>" := e (e custom com_aux) : com_scope.
> >     Notation "e" := e (in custom com_aux at level 0, e custom com) : com_scope.
> >
> >     Notation "( x )" := x (in custom com, x at level 98) : com_scope.
> >     Notation "x" := x (in custom com at level 0, x constr at level 0) :
> >     com_scope.
> >     Notation "f x .. y" := (.. (f x) .. y)
> >                       (in custom com at level 0, only parsing,
> >                       f constr at level 0, x constr at level 9,
> >                       y constr at level 9) : com_scope.
> >
> >     Notation "x + y"   := (APlus x y) (in custom com at level 50, left
> >     associativity).
> >     Notation "x - y"   := (AMinus x y) (in custom com at level 50, left
> >     associativity).
> >     Notation "x * y"   := (AMult x y) (in custom com at level 40, left
> >     associativity).
> >     Notation "'true'"  := true (at level 1).
> >     Notation "'true'"  := BTrue (in custom com at level 0).
> >     Notation "'false'" := false (at level 1).
> >     Notation "'false'" := BFalse (in custom com at level 0).
> >     Notation "x <= y"  := (BLe x y) (in custom com at level 70, no
> >     associativity).
> >     Notation "x > y"   := (BGt x y) (in custom com at level 70, no
> >     associativity).
> >     Notation "x = y"   := (BEq x y) (in custom com at level 70, no
> >     associativity).
> >     Notation "x <> y"  := (BNeq x y) (in custom com at level 70, no
> >     associativity).
> >     Notation "x && y"  := (BAnd x y) (in custom com at level 80, left
> >     associativity).
> >     Notation "'~' b"   := (BNot b) (in custom com at level 75, right
> >     associativity).
> >
> >     Locate "=".
> >     Check <{ X + Y }>.
> >     Check <{ X + Y = 0 }>.
> >     Check <{ ~ (Y = X) }>.
> >     Check <{ X + Y }>.
> >     Check <{ ~ (X + Y = Y) && Z = W }>.
> >
> >     Inductive com : Type :=
> >       | CSkip
> >       | CAsgn (x : string) (a : aexp)
> >       | CSeq (c1 c2 : com)
> >       | CIf (b : bexp) (c1 c2 : com)
> >       | CWhile (b : bexp) (c : com).
> >
> >     Notation "'skip'"  :=
> >              CSkip (in custom com at level 0) : com_scope.
> >     Notation "x := y"  :=
> >              (CAsgn x y)
> >                 (in custom com at level 0, x constr at level 0,
> >                  y at level 85, no associativity) : com_scope.
> >     Notation "x ; y" :=
> >              (CSeq x y)
> >                (in custom com at level 90,
> >                 right associativity) : com_scope.
> >     Notation "'if' x 'then' y 'else' z 'end'" :=
> >              (CIf x y z)
> >                (in custom com at level 89, x at level 98,
> >                 y at level 98, z at level 98) : com_scope.
> >     Notation "'while' x 'do' y 'end'" :=
> >              (CWhile x y)
> >                (in custom com at level 89, x at level 98,
> >                 y at level 98) : com_scope.
> >
> >     Check <{ skip }>.
> >     Check <{ (skip ; skip) ; skip }>.
> >     Check <{ 1 + 2 }>.
> >     Check <{ 2 = 1 }>.
> >     Check <{ Z := X }>.
> >     Check <{ Z := X + 3 }>.
> >     Definition func (c : com) : com := <{ c ; skip }>.
> >     Check <{ skip; func <{ skip }> }>.
> >     Definition func2 (c1 c2 : com) : com := <{ c1 ; c2 }>.
> >     Check <{ skip ; func2 <{skip}> <{skip}> }>.
> >     Check <{ true && ~(false && true) }>.
> >     Check <{ if true then skip else skip end }>.
> >     Check <{ if true && true then skip; skip else skip; X:=X+1 end }>.
> >     Check <{ while Z <> 0 do Y := Y * Z; Z := Z - 1 end }>.
> >
> >     Fixpoint aeval (st : state) (* <--- NEW *)
> >                    (a : aexp) : nat :=
> >       match a with
> >       | ANum n => n
> >       | AId x => st x                                (* <--- NEW *)
> >       | <{a1 + a2}> => (aeval st a1) + (aeval st a2)
> >       | <{a1 - a2}> => (aeval st a1) - (aeval st a2)
> >       | <{a1 * a2}> => (aeval st a1) * (aeval st a2)
> >       end.
> >
> >     Fixpoint beval (st : state) (* <--- NEW *)
> >                    (b : bexp) : bool :=
> >       match b with
> >       | <{true}>      => true
> >       | <{false}>     => false
> >       | <{a1 = a2}>   => (aeval st a1) =? (aeval st a2)
> >       | <{a1 <> a2}>  => negb ((aeval st a1) =? (aeval st a2))
> >       | <{a1 <= a2}>  => (aeval st a1) <=? (aeval st a2)
> >       | <{a1 > a2}>   => negb ((aeval st a1) <=? (aeval st a2))
> >       | <{~ b1}>      => negb (beval st b1)
> >       | <{b1 && b2}>  => andb (beval st b1) (beval st b2)
> >       end.
> >
> >     Definition Assertion := state -> Prop.
> >
> >     Definition Assert_of_bexp (b : bexp) : Assertion := fun st => beval st b =
> >     true.
> >
> >     Notation "{ P } e { Q }" :=
> >       ((Assert_of_bexp P), e, (Assert_of_bexp Q))
> >         (in custom com_aux,
> >          e custom com,
> >          P custom com,
> >          Q custom com) : com_scope.
> >
> >     Check (<{ X > 0 }>).
> >     Check (<{ X := 0 }>).
> >     Check (<{ { X > 0 } (X := 0) { true } }>).
> >     Check (<{ { X > 0 } X := 0 { true } }>).
> >
> >
> >
> >



Archive powered by MHonArc 2.6.19+.

Top of Page