Lean.Util.LeanOptions

source

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

Instances For

source

instance Lean.instInhabitedLeanOptionValue :

Inhabited LeanOptionValue

Equations

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

source

instance Lean.instReprLeanOptionValue :

Repr LeanOptionValue

Equations

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

source

def Lean.LeanOptionValue.toDataValue :

LeanOptionValue → DataValue

Equations

source

instance Lean.instValueLeanOptionValue :

KVMap.Value LeanOptionValue

Equations

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

source

instance Lean.instCoeStringLeanOptionValue :

Coe String LeanOptionValue

Equations

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

source

instance Lean.instCoeBoolLeanOptionValue :

Coe Bool LeanOptionValue

Equations

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

source

instance Lean.instCoeNatLeanOptionValue :

Coe Nat LeanOptionValue

Equations

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

source

instance Lean.instFromJsonLeanOptionValue :

FromJson LeanOptionValue

Equations

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

source

instance Lean.instToJsonLeanOptionValue :

ToJson LeanOptionValue

Equations

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

source

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

source

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.

Instances For

source

instance Lean.instInhabitedLeanOption :

Inhabited LeanOption

Equations

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

source

instance Lean.instReprLeanOption :

Repr LeanOption

Equations

Lean.instReprLeanOption = { reprPrec := Lean.reprLeanOption✝ }

source

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 ++ toString ""

source

structure Lean.LeanOptions :

Type

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

values : NameMap LeanOptionValue

Instances For

source

instance Lean.instInhabitedLeanOptions :

Inhabited LeanOptions

Equations

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

source

instance Lean.instReprLeanOptions :

Repr LeanOptions

Equations

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

source

instance Lean.instEmptyCollectionLeanOptions :

EmptyCollection LeanOptions

Equations

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

source

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

LeanOptions

Equations

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

source

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

LeanOptions

Add the options from new, overriding those in self.

Equations

self.append new = { values := Lean.RBMap.mergeBy (fun (x : Lean.Name) (x b : Lean.LeanOptionValue) => b) self.values new.values }

source

instance Lean.instAppendLeanOptions :

Append LeanOptions

Equations

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

source

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.

source

instance Lean.instHAppendLeanOptionsArrayLeanOption :

HAppend LeanOptions (Array LeanOption) LeanOptions

Equations

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

source

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

Options

Equations

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

source

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

Option LeanOptions

Equations

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

source

instance Lean.instFromJsonLeanOptions :

FromJson LeanOptions

Equations

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

source

instance Lean.instToJsonLeanOptions :

ToJson LeanOptions

Equations

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