Documentation

Lean.Elab.SetOption

source
def Lean.Elab.elabSetOption {m : Type → Type} [Monad m] [Lean.MonadOptions m] [MonadExceptOf Lean.Exception m] [Lean.MonadRef m] [Lean.AddErrorMessageContext m] [MonadLiftT (EIO Lean.Exception) m] [Lean.Elab.MonadInfoTree m] (id : Lean.Syntax) (val : Lean.Syntax) :
m Lean.Options
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.elabSetOption.setOption {m : Type → Type} [Monad m] [Lean.MonadOptions m] [MonadExceptOf Lean.Exception m] [Lean.MonadRef m] [Lean.AddErrorMessageContext m] (optionName : Lake.Name) (decl : Lean.OptionDecl) (val : Lean.DataValue) :
    m Lean.Options
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For