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)

syntax_consts
  "_replace_error" ⇌ update_error

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

end