def
Lean.Elab.validateOptionValue
{m : Type → Type}
[Monad m]
[MonadError m]
(optionName : Name)
(decl : OptionDecl)
(val : DataValue)
:
m Unit
Instances For
def
Lean.Elab.elabSetOption
{m : Type → Type}
[Monad m]
[MonadOptions m]
[MonadError m]
[MonadLiftT (EIO Exception) m]
[MonadInfoTree m]
(id val : Syntax)
:
m (Options × OptionDecl)
Elaborates id as an identifier representing an option name with value given by val, adding
appropriate info to the infotrees.
Validates that val has the correct type for values of the option id, and returns the updated
Options. Does not update the options in the monad m.
Instances For
def
Lean.Elab.checkDeprecatedOption
{m : Type → Type}
[Monad m]
[MonadOptions m]
[MonadLog m]
[AddMessageContext m]
(optionName : Name)
(decl : OptionDecl)
:
m Unit