Theory errorMonad

⊢ (∀v f. bind (return v) f = f v) ∧ ∀e f. bind (error e) f = error e

⊢ (∀v m. choice (return v) m = return v) ∧ ∀e m. choice (error e) m = m

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0.
           ∀ $var$('error').
             (∀a0.
                (∃a. a0 =
                     (λa. ind_type$CONSTR 0 (a,ARB) (λn. ind_type$BOTTOM))
                       a) ∨
                (∃a. a0 =
                     (λa.
                          ind_type$CONSTR (SUC 0) (ARB,a)
                            (λn. ind_type$BOTTOM)) a) ⇒
                $var$('error') a0) ⇒
             $var$('error') a0) rep

⊢ (∀a f f1. error_CASE (return a) f f1 = f a) ∧
  ∀a f f1. error_CASE (error a) f f1 = f1 a

⊢ (∀f f1 a. error_size f f1 (return a) = 1 + f a) ∧
  ∀f f1 a. error_size f f1 (error a) = 1 + f1 a

⊢ ∀e b. guard e b = if b then return () else error e

⊢ (∀v f. try (return v) f = return v) ∧ ∀e f. try (error e) f = f e

⊢ (∃e. P e) ⇔ (∃a. P (return a)) ∨ ∃e. P (error e)

⊢ (∀e. P e) ⇔ (∀a. P (return a)) ∧ ∀e. P (error e)

⊢ bind m f = error e ⇔ m = error e ∨ ∃u. m = return u ∧ f u = error e

⊢ bind m f = return v ⇔ ∃u. m = return u ∧ f u = return v

⊢ bind m return = m

⊢ DATATYPE (error return error)

⊢ (∀a a'. return a = return a' ⇔ a = a') ∧
  ∀a a'. error a = error a' ⇔ a = a'

⊢ ∀f0 f1. ∃fn. (∀a. fn (return a) = f0 a) ∧ ∀a. fn (error a) = f1 a

⊢ ∀M M' f f1.
    M = M' ∧ (∀a. M' = return a ⇒ f a = f' a) ∧
    (∀a. M' = error a ⇒ f1 a = f1' a) ⇒
    error_CASE M f f1 = error_CASE M' f' f1'

⊢ error_CASE x f f1 = v ⇔
  (∃a. x = return a ∧ f a = v) ∨ ∃e. x = error e ∧ f1 e = v

⊢ ∀a' a. return a ≠ error a'

⊢ ∀P. (∀a. P (return a)) ∧ (∀e. P (error e)) ⇒ ∀e. P e

⊢ ∀ee. (∃a. ee = return a) ∨ ∃e. ee = error e