structure Lean.Elab.WhereFinallyView : Type

• ref : Syntax
• tactic : TSyntax `Lean.Parser.Tactic.tacticSeq

@[instance_reducible]

instance Lean.Elab.instInhabitedWhereFinallyView : Inhabited WhereFinallyView

Equations

• Lean.Elab.instInhabitedWhereFinallyView = { default := Lean.Elab.instInhabitedWhereFinallyView.default }

def Lean.Elab.WhereFinallyView.none : WhereFinallyView

Equations

• Lean.Elab.WhereFinallyView.none = { ref := Lean.Syntax.missing, tactic := { raw := Lean.Syntax.missing } }

def Lean.Elab.WhereFinallyView.isNone (o : WhereFinallyView) : Bool

Equations

• o.isNone = (o.ref.isMissing && o.tactic.raw.isMissing)

def Lean.Elab.mkWhereFinallyView {m : Type → Type} [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Term.whereDecls) : m WhereFinallyView

Creates a view of the finally section of a whereDecls syntax object

Equations

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