class MonadDesugarerExpr (α : outParam Type) (m : Type → Type) extends MonadReaderOf (Option (CoreTLAPlus.Expression α)) m, MonadWithReaderOf (Option (CoreTLAPlus.Expression α)) m, MonadDiagnostic DesugarWarning DesugarError m, MonadFresh m : Type 1

The effects expression desugaring needs: a Reader of what @ currently refers to (none outside an EXCEPT update), error reporting, and fresh-name generation (for the tuple-pattern and multi-binder-collapse transformations, Desugarer/TLAPlus.lean).

• read : m (Option (CoreTLAPlus.Expression α))
• withReader {α : Type} (f : Option (CoreTLAPlus.Expression α) → Option (CoreTLAPlus.Expression α)) (x : m α) : m α
• tell (w : List DesugarWarning) : m PUnit.{1}
• listen {α : Type} (f : m α) : m (α × List DesugarWarning)
• pass {α : Type} (f : m (α × (List DesugarWarning → List DesugarWarning))) : m α
• throw {α : Type} : DesugarError → m α
• tryCatch {α : Type} (body : m α) (handler : DesugarError → m α) : m α
• fresh : m ℕ