Theory Certification_Monads.Error_Syntax

(* Title:    Error_Syntax  
   Author:   Christian Sternagel
*)

section ‹Try-Catch and Error-Update Notation for Arbitrary Types›

theory Error_Syntax
imports
  Main
  "HOL-Library.Adhoc_Overloading"
begin

consts
  catch :: "'a ⇒ ('b ⇒ 'c) ⇒ 'c" ("(try(/ _)/ catch(/ _))" [12, 12] 13)
  update_error :: "'a ⇒ ('b ⇒ 'c) ⇒ 'd" (infixl "<+?" 61)

syntax
  "_replace_error" :: "'a ⇒ 'b ⇒ 'a" (infixl "<?" 61)

translations
  "m <? e" ⇀ "m <+? (λ_. e)"

end