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