Documentation

Lean.Elab.WhereFinally

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