Theory Refine_Monadic_Syntax_Sugar

section ‹Additional Syntactic Sugar for Refinement›
(* TODO: Move to Refine_Monadic folder, include in Refine_Monadic *)
theory Refine_Monadic_Syntax_Sugar
imports Refine_Monadic
begin

  locale Refine_Monadic_Syntax begin
  
    notation SPEC (binder "spec " 10)
    notation ASSERT ("assert")
    notation RETURN ("return")
    notation FOREACH ("foreach")
    notation WHILE ("while")
    notation WHILET ("while⇩T")
    notation WHILEI ("while⇗_⇖")
    notation WHILET ("while⇩T")
    notation WHILEIT ("while⇩T⇗_⇖")

    notation RECT (binder "rec⇩T " 10)
    notation REC (binder "rec " 10)

  end
end