Documentation

Lean.Elab.WhereFinally

source
structure Lean.Elab.WhereFinallyView :
Type
Instances For
    source
    @[instance_reducible]
    instance Lean.Elab.instInhabitedWhereFinallyView :
    Inhabited WhereFinallyView
    source
    def Lean.Elab.WhereFinallyView.none :
    WhereFinallyView
    Instances For
      source
      def Lean.Elab.WhereFinallyView.isNone (o : WhereFinallyView) :
      Bool
      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

        Instances For