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 (s : String) : LeanOptionValue
• ofBool (b : Bool) : LeanOptionValue
• ofNat (n : Nat) : LeanOptionValue

instance Lean.instInhabitedLeanOptionValue : Inhabited LeanOptionValue

Equations

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

def Lean.instInhabitedLeanOptionValue.default : LeanOptionValue

Equations

• Lean.instInhabitedLeanOptionValue.default = Lean.LeanOptionValue.ofString default

instance Lean.instReprLeanOptionValue : Repr LeanOptionValue

Equations

• Lean.instReprLeanOptionValue = { reprPrec := Lean.instReprLeanOptionValue.repr }

def Lean.instReprLeanOptionValue.repr : LeanOptionValue → Nat → Format

Equations

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

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

Equations

• Lean.LeanOptionValue.ofDataValue? (Lean.DataValue.ofString s) = some (Lean.LeanOptionValue.ofString s)
• Lean.LeanOptionValue.ofDataValue? (Lean.DataValue.ofBool b) = some (Lean.LeanOptionValue.ofBool b)
• Lean.LeanOptionValue.ofDataValue? (Lean.DataValue.ofNat n) = some (Lean.LeanOptionValue.ofNat n)
• Lean.LeanOptionValue.ofDataValue? x✝ = none

def Lean.LeanOptionValue.toDataValue : LeanOptionValue → DataValue

Equations

• (Lean.LeanOptionValue.ofString a).toDataValue = Lean.DataValue.ofString a
• (Lean.LeanOptionValue.ofBool a).toDataValue = Lean.DataValue.ofBool a
• (Lean.LeanOptionValue.ofNat a).toDataValue = Lean.DataValue.ofNat a

instance Lean.instValueLeanOptionValue : KVMap.Value LeanOptionValue

Equations

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

instance Lean.instCoeStringLeanOptionValue : Coe String LeanOptionValue

Equations

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

instance Lean.instCoeBoolLeanOptionValue : Coe Bool LeanOptionValue

Equations

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

instance Lean.instCoeNatLeanOptionValue : Coe Nat LeanOptionValue

Equations

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

instance Lean.instFromJsonLeanOptionValue : FromJson LeanOptionValue

Equations

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

instance Lean.instToJsonLeanOptionValue : ToJson LeanOptionValue

Equations

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

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

Formats the lean option value as a CLI flag argument.

Equations

• (Lean.LeanOptionValue.ofString a).asCliFlagValue = toString "\"" ++ toString a ++ toString "\""
• (Lean.LeanOptionValue.ofBool a).asCliFlagValue = toString a
• (Lean.LeanOptionValue.ofNat a).asCliFlagValue = toString a

structure Lean.LeanOption : Type

An option that is used by Lean as if it was passed using -D.

• name : Name

  The option's name.

• value : LeanOptionValue

  The option's value.

instance Lean.instInhabitedLeanOption : Inhabited LeanOption

Equations

• Lean.instInhabitedLeanOption = { default := Lean.instInhabitedLeanOption.default }

def Lean.instInhabitedLeanOption.default : LeanOption

Equations

• Lean.instInhabitedLeanOption.default = { name := default, value := default }

instance Lean.instReprLeanOption : Repr LeanOption

Equations

• Lean.instReprLeanOption = { reprPrec := Lean.instReprLeanOption.repr }

def Lean.instReprLeanOption.repr : LeanOption → Nat → Format

Equations

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

def Lean.LeanOption.asCliArg (o : LeanOption) : String

Formats the lean option as a CLI argument using the -D flag.

Equations

• o.asCliArg = toString "-D" ++ toString o.name ++ toString "=" ++ toString o.value.asCliFlagValue

structure Lean.LeanOptions : Type

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

• values : NameMap LeanOptionValue

instance Lean.instInhabitedLeanOptions : Inhabited LeanOptions

Equations

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

def Lean.instInhabitedLeanOptions.default : LeanOptions

Equations

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

def Lean.instReprLeanOptions.repr : LeanOptions → Nat → Format

Equations

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

instance Lean.instReprLeanOptions : Repr LeanOptions

Equations

• Lean.instReprLeanOptions = { reprPrec := Lean.instReprLeanOptions.repr }

instance Lean.instEmptyCollectionLeanOptions : EmptyCollection LeanOptions

Equations

• Lean.instEmptyCollectionLeanOptions = { emptyCollection := { values := ∅ } }

def Lean.LeanOptions.ofArray (opts : Array LeanOption) : LeanOptions

Equations

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

def Lean.LeanOptions.append (self new : LeanOptions) : LeanOptions

Add the options from new, overriding those in self.

Equations

• self.append new = { values := Std.TreeMap.mergeWith (fun (x : Lean.Name) (x b : Lean.LeanOptionValue) => b) self.values new.values }

instance Lean.instAppendLeanOptions : Append LeanOptions

Equations

• Lean.instAppendLeanOptions = { append := Lean.LeanOptions.append }

def Lean.LeanOptions.appendArray (self : LeanOptions) (new : Array LeanOption) : LeanOptions

Add the options from new, overriding those in self.

Equations

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

instance Lean.instHAppendLeanOptionsArrayLeanOption : HAppend LeanOptions (Array LeanOption) LeanOptions

Equations

• Lean.instHAppendLeanOptionsArrayLeanOption = { hAppend := Lean.LeanOptions.appendArray }

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

Equations

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

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

Equations

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

instance Lean.instFromJsonLeanOptions : FromJson LeanOptions

Equations

• Lean.instFromJsonLeanOptions = { fromJson? := fun (j : Lean.Json) => Lean.LeanOptions.mk <$> Lean.fromJson? j }

instance Lean.instToJsonLeanOptions : ToJson LeanOptions

Equations

• Lean.instToJsonLeanOptions = { toJson := fun (options : Lean.LeanOptions) => Lean.toJson options.values }