Exception Postcondition Types

Heterogeneous lists of exception postconditions for monads with multiple exception layers.

An EPost is a type-level list that tracks postconditions for each exception type in a monad transformer stack. For example, ExceptT Nat (ExceptT String (StateM σ)) would use EPost⟨Nat → σ → Prop, String → σ → Prop⟩ to specify postconditions for both exception types.

Overview

• EPost.Nil is the empty exception postcondition (no exceptions).
• EPost.Cons eh et pairs a head postcondition type eh with a tail et.
• EPost⟨e₁, e₂, ...⟩ is notation for nested EPost.Cons.
• epost⟨v₁, v₂, ...⟩ is notation for constructing exception postcondition values.

structure Std.Internal.Do.EPost.Nil : Type

The empty exception postcondition type, used when a monad has no exception layers.

structure Std.Internal.Do.EPost.Cons (eh : Type u) (et : Type v) : Type (max u v)

A cons cell pairing a head exception postcondition type eh with a tail et.

For a monad with exception type ε over lattice l, the head eh is typically ε → l and the tail et tracks remaining exception layers.

• head : eh

  The head exception postcondition.

• tail : et

  The tail exception postconditions.

Partial Order and Complete Lattice Instances

Exception postconditions are ordered componentwise: p ⊑ q iff each component of p is below the corresponding component of q.

@[implicit_reducible]

instance Std.Internal.Do.instPartialOrderNil : Lean.Order.PartialOrder EPost⟨⟩

The trivial partial order on EPost.Nil: all values are equal.

Equations

• Std.Internal.Do.instPartialOrderNil = { rel := fun (x x_1 : EPost⟨⟩) => True, rel_refl := ⋯, rel_trans := ⋯, rel_antisymm := ⋯ }

@[implicit_reducible]

instance Std.Internal.Do.instCompleteLatticeNil : Lean.Order.CompleteLattice EPost⟨⟩

The trivial complete lattice on EPost.Nil.

Equations

• Std.Internal.Do.instCompleteLatticeNil = { toPartialOrder := Std.Internal.Do.instPartialOrderNil, has_sup := Std.Internal.Do.instCompleteLatticeNil._proof_1 }

@[implicit_reducible]

instance Std.Internal.Do.instPartialOrderCons {eh : Type u_1} {et : Type u_2} [Lean.Order.PartialOrder eh] [Lean.Order.PartialOrder et] : Lean.Order.PartialOrder (EPost.Cons✝ eh et)

Componentwise partial order on EPost.Cons, via PProd.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Internal.Do.instCompleteLatticeCons {eh : Type u_1} {et : Type u_2} [Lean.Order.CompleteLattice eh] [Lean.Order.CompleteLattice et] : Lean.Order.CompleteLattice (EPost.Cons✝ eh et)

Componentwise complete lattice on EPost.Cons, via PProd.

Equations

• Std.Internal.Do.instCompleteLatticeCons = { toPartialOrder := Std.Internal.Do.instPartialOrderCons, has_sup := ⋯ }

Ordering Lemmas

theorem Std.Internal.Do.EPost.Cons.le_head {eh : Type u_1} {et : Type u_2} [Lean.Order.PartialOrder eh] [Lean.Order.PartialOrder et] {p q : EPost.Cons✝ eh et} (h : Lean.Order.PartialOrder.rel p q) : Lean.Order.PartialOrder.rel p.head q.head

Extract a head ordering from an EPost.Cons ordering.

theorem Std.Internal.Do.EPost.Cons.le_tail {eh : Type u_1} {et : Type u_2} [Lean.Order.PartialOrder eh] [Lean.Order.PartialOrder et] {p q : EPost.Cons✝ eh et} (h : Lean.Order.PartialOrder.rel p q) : Lean.Order.PartialOrder.rel p.tail q.tail

Extract a tail ordering from an EPost.Cons ordering.

theorem Std.Internal.Do.EPost.Cons.mk_le {e : Type u_1} {e' : Type u_2} [Lean.Order.PartialOrder e] [Lean.Order.PartialOrder e'] (eposth : e) (epostt : e') (epost : EPost.Cons✝ e e') : Lean.Order.PartialOrder.rel eposth epost.head → Lean.Order.PartialOrder.rel epostt epost.tail → Lean.Order.PartialOrder.rel (EPost.Cons.mk✝ eposth epostt) epost

An EPost.Cons value is below another if both components are below.

theorem Std.Internal.Do.EPost.Cons.mk_le_tail {e : Type u_1} {e' : Type u_2} [Lean.Order.PartialOrder e] [Lean.Order.PartialOrder e'] (epostt : e') (epost : EPost.Cons✝ e e') : Lean.Order.PartialOrder.rel epostt epost.tail → Lean.Order.PartialOrder.rel (EPost.Cons.mk✝ epost.head epostt) epost

An EPost.Cons value is below another if both components are below.

theorem Std.Internal.Do.EPost.Nil.le (epost : EPost⟨⟩) : Lean.Order.PartialOrder.rel epost⟨⟩ epost

The unique EPost.Nil value is below any EPost.Nil value.

theorem Std.Internal.Do.EPost.Cons.head_bot {eh : Type u} {et : Type v} [Lean.Order.CompleteLattice eh] [Lean.Order.CompleteLattice et] : Lean.Order.bot.head = Lean.Order.bot

The head component of the bottom EPost.Cons is the bottom element. Propositional (not definitional), because ⊥ of a complete lattice is csup ∅, not a constructor application.

Notation

• EPost⟨e₁, e₂, ...⟩ builds an exception postcondition type (nested EPost.Cons).
• epost⟨v₁, v₂, ...⟩ builds an exception postcondition value (nested EPost.Cons.mk).

def Std.Internal.Do.«termEPost⟨_⟩» : Lean.ParserDescr

Exception postcondition type notation: EPost⟨ε₁ → l, ε₂ → l⟩ for nested EPost.Cons.

Equations

• One or more equations did not get rendered due to their size.

def Std.Internal.Do.«termEpost⟨_⟩» : Lean.ParserDescr

Exception postcondition value notation: epost⟨h₁, h₂⟩ for nested EPost.Cons.mk.

Equations

• One or more equations did not get rendered due to their size.

def Std.Internal.Do.unexpandEPostNil : Lean.PrettyPrinter.Unexpander

Pretty-print EPost.Nil as EPost⟨⟩.

Equations

• One or more equations did not get rendered due to their size.

def Std.Internal.Do.unexpandEPostCons : Lean.PrettyPrinter.Unexpander

Pretty-print EPost.Cons as EPost⟨e₁, e₂, ...⟩.

Equations

• One or more equations did not get rendered due to their size.

def Std.Internal.Do.unexpandEPostNilMk : Lean.PrettyPrinter.Unexpander

Pretty-print EPost.Nil.mk as epost⟨⟩.

Equations

• One or more equations did not get rendered due to their size.

def Std.Internal.Do.unexpandEPostConsMk : Lean.PrettyPrinter.Unexpander

Pretty-print EPost.Cons.mk as epost⟨v₁, v₂, ...⟩.

Equations

• One or more equations did not get rendered due to their size.