Documentation

Lean.Elab.SetOption

def Lean.Elab.elabSetOption {m : TypeType} [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
def Lean.Elab.elabSetOption.setOption {m : TypeType} [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