def
Lean.Elab.validateOptionValue
{m : Type → Type}
[Monad m]
[MonadError m]
(optionName : Name)
(decl : OptionDecl)
(val : DataValue)
:
m Unit
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- One or more equations did not get rendered due to their size.