inductive Lean.LeanOptionValue : Type

Restriction of DataValue that covers exactly those cases that Lean is able to handle when passed via the -D flag.

• ofString: String → Lean.LeanOptionValue
• ofBool: Bool → Lean.LeanOptionValue
• ofNat: Nat → Lean.LeanOptionValue

Instances For

• Lean.instCoeBoolLeanOptionValue
• Lean.instCoeNatLeanOptionValue
• Lean.instCoeStringLeanOptionValue
• Lean.instFromJsonLeanOptionValue
• Lean.instInhabitedLeanOptionValue
• Lean.instReprLeanOptionValue
• Lean.instToJsonLeanOptionValue
• Lean.instValueLeanOptionValue

instance Lean.instInhabitedLeanOptionValue : Inhabited Lean.LeanOptionValue

Equations

• Lean.instInhabitedLeanOptionValue = { default := Lean.LeanOptionValue.ofString default }

instance Lean.instReprLeanOptionValue : Repr Lean.LeanOptionValue

Equations

• Lean.instReprLeanOptionValue = { reprPrec := Lean.reprLeanOptionValue✝ }

def Lean.LeanOptionValue.ofDataValue? : Lean.DataValue → Option Lean.LeanOptionValue

Equations

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

def Lean.LeanOptionValue.toDataValue : Lean.LeanOptionValue → Lean.DataValue

Equations

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

instance Lean.instValueLeanOptionValue : Lean.KVMap.Value Lean.LeanOptionValue

Equations

• Lean.instValueLeanOptionValue = { toDataValue := Lean.LeanOptionValue.toDataValue, ofDataValue? := Lean.LeanOptionValue.ofDataValue? }

instance Lean.instCoeStringLeanOptionValue : Coe String Lean.LeanOptionValue

Equations

• Lean.instCoeStringLeanOptionValue = { coe := Lean.LeanOptionValue.ofString }

instance Lean.instCoeBoolLeanOptionValue : Coe Bool Lean.LeanOptionValue

Equations

• Lean.instCoeBoolLeanOptionValue = { coe := Lean.LeanOptionValue.ofBool }

instance Lean.instCoeNatLeanOptionValue : Coe Nat Lean.LeanOptionValue

Equations

• Lean.instCoeNatLeanOptionValue = { coe := Lean.LeanOptionValue.ofNat }

instance Lean.instFromJsonLeanOptionValue : Lean.FromJson Lean.LeanOptionValue

Equations

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

instance Lean.instToJsonLeanOptionValue : Lean.ToJson Lean.LeanOptionValue

Equations

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

def Lean.LeanOptionValue.asCliFlagValue (v : Lean.LeanOptionValue) : String

Formats the lean option value as a CLI flag argument.

Equations

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

structure Lean.LeanOptions : Type

Options that are used by Lean as if they were passed using -D.

• values : Lean.RBMap Lake.Name Lean.LeanOptionValue Lean.Name.cmp

Instances For

• Lean.instFromJsonLeanOptions
• Lean.instInhabitedLeanOptions
• Lean.instReprLeanOptions
• Lean.instToJsonLeanOptions

instance Lean.instInhabitedLeanOptions : Inhabited Lean.LeanOptions

Equations

• Lean.instInhabitedLeanOptions = { default := { values := default } }

instance Lean.instReprLeanOptions : Repr Lean.LeanOptions

Equations

• Lean.instReprLeanOptions = { reprPrec := Lean.reprLeanOptions✝ }

def Lean.LeanOptions.toOptions (leanOptions : Lean.LeanOptions) : Lean.Options

Equations

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

def Lean.LeanOptions.fromOptions? (options : Lean.Options) : Option Lean.LeanOptions

Equations

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

instance Lean.instFromJsonLeanOptions : Lean.FromJson Lean.LeanOptions

Equations

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

instance Lean.instToJsonLeanOptions : Lean.ToJson Lean.LeanOptions

Equations

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