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