Documentation

Lean.Elab.SetOption

source
def Lean.Elab.elabSetOption {m : Type → Type} [Monad m] [MonadOptions m] [MonadError m] [MonadLiftT (EIO Exception) m] [MonadInfoTree m] (id val : Syntax) :
m Options
Equations
    Instances For
      source
      def Lean.Elab.elabSetOption.setOption {m : Type → Type} [Monad m] [MonadOptions m] [MonadError m] (optionName : Name) (decl : OptionDecl) (val : DataValue) :
      m Options
      Equations
        Instances For