Exception Postcondition Stack Notation

A monad transformer stack carries one exception postcondition for each transformer that throws. A stack of postconditions is a right-nested × chain with the marker type EStackEnd as its last component. EStack⟨Nat → σ → Prop, String → σ → Prop⟩ is the stack of ExceptT Nat (ExceptT String (StateM σ)), and estack⟨e₁, e₂⟩ is a value of it. The notation hides the nesting and the markers. EStackEnd and EStackEnd.mk are abbreviations of Unit and (), so the unexpanders can recognize a stack while every Unit instance still applies.

A base monad has one exception postcondition and no stack, so it does not use the notation: Except ε carries a bare ε → Prop.

@[reducible, inline]

abbrev Std.WP.EStackEnd : Type

The last component of an exception postcondition stack. It reduces to Unit, so every Unit instance applies. It is a named constant, so only a stack prints as EStack⟨…⟩.

Equations

• EStack⟨⟩ = Unit

@[reducible, inline]

abbrev Std.WP.EStackEnd.mk : EStack⟨⟩

The value of the last stack component. It reduces to (). It is a named constant, so only a stack value prints as estack⟨…⟩.

Equations

• estack⟨⟩ = ()

def Std.WP.«termEStack⟨_⟩» : Lean.ParserDescr

Exception postcondition stack type: EStack⟨ε₁ → l, ε₂ → l⟩ is (ε₁ → l) × (ε₂ → l) × EStack⟨⟩.

Equations

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

def Std.WP.«termEstack⟨_⟩» : Lean.ParserDescr

Exception postcondition stack value: estack⟨e₁, e₂⟩ is (e₁, e₂, ()).

Equations

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

def Std.WP.unexpandEStackEnd : Lean.PrettyPrinter.Unexpander

Prints EStackEnd as EStack⟨⟩.

Equations

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

def Std.WP.unexpandEStack : Lean.PrettyPrinter.Unexpander

Prints a product that ends in EStack⟨⟩ as EStack⟨e₁, e₂, …⟩.

Equations

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

def Std.WP.unexpandEStackEndMk : Lean.PrettyPrinter.Unexpander

Prints EStackEnd.mk as estack⟨⟩.

Equations

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

def Std.WP.unexpandEStackMk : Lean.PrettyPrinter.Unexpander

Prints a tuple that ends in estack⟨⟩ as estack⟨e₁, e₂, …⟩.

Equations

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