source
structure Lean.Elab.WhereFinallyView :
Type

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

Instances For

source
instance Lean.Elab.instInhabitedWhereFinallyView :
Inhabited WhereFinallyView
Equations

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

source
def Lean.Elab.instInhabitedWhereFinallyView.default :
WhereFinallyView
Equations

- Lean.Elab.instInhabitedWhereFinallyView.default = { ref := default, tactic := default }

Instances For

source
def Lean.Elab.WhereFinallyView.none :
WhereFinallyView
Equations

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

Instances For

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

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

Instances For

source
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.

Instances For