opaque Lean.Elab.linter.deprecated.options : Lean.Option Bool

def Lean.Elab.validateOptionValue {m : Type → Type} [Monad m] [MonadError m] (optionName : Name) (decl : OptionDecl) (val : DataValue) : m Unit

Equations

• Lean.Elab.validateOptionValue optionName decl val = if decl.defValue.sameCtor val = true then pure () else Lean.Elab.validateOptionValue.throwMistypedOptionValue✝ optionName val decl.defValue

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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.checkDeprecatedOption {m : Type → Type} [Monad m] [MonadOptions m] [MonadLog m] [AddMessageContext m] (optionName : Name) (decl : OptionDecl) : m Unit

Equations

• One or more equations did not get rendered due to their size.