refinement-parsers.fmt

%if style == poly
%format (Forall(a)) = "\!\!"
%format (implicit(a)) = "\!\!"
%format (hidden(a)) = "\!\!"
%format (hiddenArg(a)) = "\_"
%format (hiddenInstance(a)) = "\!\!"
%format (ldotsHere(a)) = "\ldots"
%format (hiddenConst (a)) = a
%format (Exists (a) (b) (c)) = "\exists\ (" a "\ :\ " b ")\ \to\ " c
%format (equiv (a) (b) (c)) = b "\equiv" c
%format (equiv' (a) (b) (c)) = b "\equiv" c
%format (equivStep (a) (b) (c) (d) (e) (f)) = ≡-step "\ " (f)
%format N = "\mathbb{N}"
%format e1 = e "_1"
%format e2 = e "_2"
%format v1 = v "_1"
%format v2 = v "_2"
%format x1 = x "_1"
%format x2 = x "_2"
%format t1 = t "_1"
%format t2 = t "_2"
%format s1 = s "_1"
%format s2 = s "_2"
%format c1 = c "_1"
%format c1, = c "_1,"
%format c2 = c "_2"
%format c2, = c "_2,"
%format f1 = f "_1"
%format f2 = f "_2"
%format g1 = g "_1"
%format g2 = g "_2"
%format i1 = i "_1"
%format i2 = i "_2"
%format nd1 = nd "_1"
%format nd2 = nd "_2"
%format pt1 = pt "_1"
%format pt2 = pt "_2"
%format law1 = law "_1"
%format law2 = law "_2"
%format law3 = law "_3"
%format law4 = law "_4"
%format top = "\top"
%format <-> = "\leftrightarrow"
%format refines = "\sqsubseteq"
%format elem = "\in"
%format wpEval = wp "_{" eval "}"
%format wpCR = wp
%format _tril_ = "\_\triangleleft\_"
%format tril = "\triangleleft"
%format _trir_ = "\_\triangleright\_"
%format trir = "\triangleright"
%format maxPost' = maxPost
%format maxSpec' = maxSpec
%format if' = if
%format ^^ = "\;"
%format Set1 = Set
%format forall = "\forall"
%format _>>=_ = "\_\!\bind\!\_"
%format _>=>_ = "\_\!>\!\!\!\!\mathbin{=}\!\!\!\!>\!\_"
%format >=> = ">\!\!\!\!\mathbin{=}\!\!\!\!>"
%format constructor = "\Keyword{constructor}"
%format wpState' = wpState
%format statePT' = statePT
%format (spec (a) (b)) = "\mathbin{[}" a "\mathbin{,}" b "\mathbin{]}"
%format spec' = "[\_,\_]"
%format [[ = "["
%format ]] = "]"
%format ]]F = "]^F"
%format ]]S = "]^S"
%format [[_,_]] = "[\_,\_]"
%format [[_,_]]F = "[\_,\_]^F"
%format [[_,_]]S = "[\_,\_]^S"
%format SpecF = "\text{\itshape Spec}^F"
%format wpSpecF = "\text{\itshape wpSpec}^F"
%format correctnessAdd = correctness
%format correctnessProduct = correctness
%format correctnessRelabel = correctness
%format f91-partial-correctness = corectness
%format forall = "\forall"
%format Sigma = "\sum"
%format (seq (a) (b)) = "[" a "\ldots" a "+" b "]"
%format (instantiate (a)) = " " a " "
%format relabelSpec1 = relabelSpec "_1"
%format relabelSpec2 = relabelSpec "_2"
%format ~> = "\looparrowright"
%format _~>_ = "\_\looparrowright\_"
%format RecArr' = "\_\overset{\_}{\looparrowright}\_"
%format (RecArr (a) (b) (c)) = a "\overset{" b "}{\looparrowright}" c
%format (RecArrBinding (x) (a) (b) (c)) = (x ":" a) "\overset{" b "}{\looparrowright}" c
%format Nat = "\N"
%format λ = "\lambda"
%format ∀ = "\forall"
%format (underlying (a)) = a
%format ⊑ = "\sqsubseteq"
%format _⊑_ = "\_\!\sqsubseteq\!\_"
%format PTS = "\text{\itshape PT}^S"
%format PTSs = "\text{\itshape PTs}^S"
%format SpecS = "\text{\itshape Spec}^S"
%format ptRecS = "\text{\itshape ptRec}^S"
%format ⊑S = "\sqsubseteq^S"
%format _⊑S_ = "\_\!\sqsubseteq^S\!\_"
%format :+: = ":\!\!+\!\!:"
%format _:+:_ = "\_\!" :+: "\!\_"
%format :: = "::"
%format _::_ = "\_\!" :: "\!\_"
%format ∘ = "\circ"
%format _∘_ = "\_\!\circ\!\_"
%format == = "=="
%format _==_ = "\_\!==\!\_"
%format -> = "\to"
%format → = "\to"
%format ⊤ = "\top"
%format ⊥ = "\bot"
%format ∈ = "\in"
%format _∈_ = "\_\!\in\!\_"
%format + = "\mathbin{+}"
%format _+_ = "\_\!" + "\!\_"
%format < = "\mathbin{<}"
%format _<_ = "\_\!" < "\!\_"
%format <? = "\mathbin{\smash{\overset{\raisebox{-0.3em}{\tiny ?}}{<}}}"
%format _<?_ = "\_\!" <? "\!\_"
%format >? = "\mathbin{\smash{\overset{\raisebox{-0.2em}{\tiny ?}}{>}}}"
%format _>?_ = "\_\!" >? "\!\_"
%format ≥? = "\mathbin{\smash{\overset{\raisebox{-0.2em}{\tiny ?}}{\ge}}}"
%format _≥?_ = "\_\!" ≥? "\!\_"
%format ≟ = "\mathbin{\smash{\overset{\raisebox{-0.2em}{\tiny ?}}{=}}}"
%format (primCharEquality(a)(b)) = a ≟ b
%format ≟n = ≟
%format _≟n_ = "\_\!" ≟n "\!\_"
%format ≤ = "\mathbin{\le}"
%format _≤_ = "\_\!\mathbin{\le}\!\_"
%format - = "\mathbin{-}"
%format _-_ = "\_\!\mathbin{_}\!\_"
%format ≺ = "\mathbin{\prec}"
%format _≺_ = "\_\!\mathbin{\prec}\!\_"
%format Termination._≺_ = Termination. "\_\!\mathbin{\prec}\!\_"
%format ⇔ = "\mathbin{\iff}"
%format _⇔_ = "\_\!\mathbin{\iff}\!\_"
%format ∧ = "\mathbin{\wedge}"
%format ∨ = "\mathbin{\vee}"
%format _∣_ = "\_\!\mathbin{\mid}\!\_"
%format ∣ = "\mathbin{\mid}"
%format ⊑-refl = "\sqsubseteq\!\text{\itshape-refl}"
%format ⊑-trans = "\sqsubseteq\!\text{\itshape-trans}"
%format ⊑S-refl = "\sqsubseteq\!\text{\itshape-refl}"
%format ⊑S-reflexivity = "\sqsubseteq\!\text{\itshape-reflexivity}"
%format ⊑S-trans = "\sqsubseteq\!\text{\itshape-trans}"
%format !! = "\todo{\text{Finish the proof!}}"
%format do = "\textrm{\bfseries do}"
%format if = "\textrm{\bfseries if}"
%format then = "\textrm{\bfseries then}"
%format else = "\textrm{\bfseries else}"
%format ⦃ = "\{\!\!\{\!"
%format ⦄ = "\!\}\!\!\}"
%format ∈Head = "\in\!\mathit{Head}"
%format ∈Tail = "\in\!\mathit{Tail}"
%format ≡ = "\equiv"
%format _≡_ = "\_\!\equiv\!\_"
%format ≡-step = "\equiv\text{-step}"
%format hiddenT = "\!"
%format hrule = "\midrule"
%format (primStringToList a) = a
%format epsilonPart = "\varepsilon\text{\itshape Part}"
%format epsilonPartGivesEpsilon = "\varepsilon\text{\itshape PartSound}"
%format epsilonPartCorrect = "\varepsilon\text{\itshape PartComplete}"
%format matchEpsilon = "\varepsilon?"
%format ε = "\varepsilon?"
%format ⟦ = "\llbracket"
%format ⟧ = "\rrbracket"
%format ∥ = "\|"
%format ⟦_⟧ = ⟦ "\!\_\!" ⟧
%format ⟦_∥_⟧ = ⟦ "\!\_\!" ∥ "\!\_\!" ⟧
%format _∈[_] = "\_\! \in \![\_]"
%format ∈[ = "\in["
%format _,_=>_ = "\_\!" , "\!\_\!" => "\!\_"
%format _⊢_∈⟦_⟧=>_,_ = "\_\!" ⊢ "\!\_\!" ∈⟦ "\!\_\!" ⟧=> "\!\_\!" , "\!\_"
%format _⊢_~_=>_,_ = "\_\!" ⊢ "\!\_\!" ~ "\!\_\!" => "\!\_\!" , "\!\_"
%format ⊢ = "\vdash"
%format ∈⟦ = "\in \llbracket"
%format ⟧=> = "\rrbracket \Rightarrow"
%format ~ = "\sim"
%format ≥ = "\geq"
%format ⌊ = "\lfloor"
%format /2⌋ = "/2~\rfloor"
%format ⌋ = "\rfloor"
%format ∈ = "\in"
%format × = "\times"
%format ⊆ = "\subseteq"
%format ∪ = "\cup"
%format ∪t = "\cup"
%format _∪t_ = "\_\!" ∪t "\!\_"
%format ≡ = "\equiv"
%format ⇔ = "\iff"
%format _⇔_ = "\_\!" ⇔ "\!\_"
%format ⇔-refl = "\mathit{\iff\!\text{-}refl}"
%format converseCompositionalitySpec = "\text{\itshape compositionalitySpec}^\prime"
%format ≤-reflexive = "\text{\itshape $\le$-reflexive}"
%format ≤-refl = "\text{\itshape $\le$-refl}"
%format ≤-trans = "\text{\itshape $\le$-trans}"
%format ≤-step = "\text{\itshape $\le$-step}"
%format +-identityʳ = "\text{\itshape +-zero}"
%format <⇒≱ = "<\rightarrow\not\ge"
%format s≤s = "s\!\le\!s"
%format z≤n = "z\!\le\!n"
%format tree = "\mathit{Tree}"
%format <$> = "\langle\$\rangle"
%format terminates-in = "\mathit{terminates\text{-}in}"
%format terminates-fmap = "\mathit{terminates\text{-}fmap}"
%format == = "\equiv"
%format · = "\cdot"
%format _·_ = "\_\!\cdot\!\_"
%format (wp (a) (b)) = "\llbracket" b "\rrbracket_{" a "}"
%format (wp' (a)) = "\llbracket \_ \rrbracket_{" a "}"
%format wp'' = "\llbracket \_ \rrbracket"
%format (wpS (a) (b)) = "\llbracket" b "\rrbracket^S_{" a "}"
%format wpS' = "\llbracket \_ \rrbracket^S"
%format (wpNondetAll (b)) = "\llbracket" b "\rrbracket_{\text{all}}"
%format wpNondetAll' = "\llbracket \_ \rrbracket_{\text{all}}"
%format (wpMatch (b)) = "\llbracket" b "\rrbracket_{\text{match}}"
%format (wpMatch') = "\llbracket \_ \rrbracket_{\text{match}}"
%format (wpSpec [[ pre , post ]]) = "\llbracket" pre "," post "\rrbracket_{\text{spec}}"
%format wpSpec' = "\llbracket \_ , \_ \rrbracket_{\text{spec}}"
%format (wpFromProd (a) (b)) = "\llbracket" b "\rrbracket_{\text{fromProd}}\ " a
%format Set₁ = Set
%format hasNo* = "\mathit{hasNo\star}"
%else
%format (Forall (a)) = "forall { " a " } -> "
%format (Exists (a) (b) (c)) = "Sigma " (b) " \ " a " -> " (c)
%format (implicit(a)) = "{" a "} ->"
%format (hidden(a)) = "{" a "}"
%format (hiddenInstance(a)) = "⦃ " a " ⦄"
%format (hiddenArg(a)) = "(" a ")"
%format (instantiate (a)) = "(" a " {a})"
%format (hiddenConst (a)) = "(\_ -> " a ")"
%format (ldotsHere(a)) = a
%format N = "Nat"
%format top = "⊤"
%format ^^ = " "
%format _tril_ = _▹_
%format tril = ▹
%format _trir_ = _◃_
%format trir = ◃
%format RecArr = "RecArr"
%format (RecArrBinding (x) (a) (b) (c)) = ("RecArr" (a) (b) " λ " (x) " → " (c))
%format RecArr' = "RecArr"
%format equivStep = ≡-step
%format hiddenT = ⊤
%format spec' = spec
%format (wp a b) = "wp" a b
%format wp' = "wp"
%format wp'' = "wp"
%format (wpMatch b) = "wpMatch" b
%format wpMatch' = "wpMatch"
%format (wpNondetAll b) = "wpNondetAll" b
%format wpNondetAll' = "wpNondetAll"
%format (wpS a b) = "wpS" a b
%format wpS' = "wpS"
%format (wpSpec s) = "wpSpec" s
%format wpSpec' = "wpSpec"
%endif