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

source

instance Lean.instReprLeanOptionValue :

Repr LeanOptionValue

Equations

source

def Lean.LeanOptionValue.ofDataValue? :

DataValue → Option LeanOptionValue

Equations

Instances For

source

def Lean.LeanOptionValue.toDataValue :

LeanOptionValue → DataValue

Equations

Instances For

source

instance Lean.instValueLeanOptionValue :

KVMap.Value LeanOptionValue

Equations

source

instance Lean.instCoeStringLeanOptionValue :

Coe String LeanOptionValue

Equations

source

instance Lean.instCoeBoolLeanOptionValue :

Coe Bool LeanOptionValue

Equations

source

instance Lean.instCoeNatLeanOptionValue :

Coe Nat LeanOptionValue

Equations

source

instance Lean.instFromJsonLeanOptionValue :

FromJson LeanOptionValue

Equations

source

instance Lean.instToJsonLeanOptionValue :

ToJson LeanOptionValue

Equations

source

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

String

Formats the lean option value as a CLI flag argument.

Equations

Instances For

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

source

instance Lean.instReprLeanOptions :

Repr LeanOptions

Equations

source

instance Lean.instEmptyCollectionLeanOptions :

EmptyCollection LeanOptions

Equations

source

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

Options

Equations

Instances For

source

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

Option LeanOptions

Equations

Instances For

source

instance Lean.instFromJsonLeanOptions :

FromJson LeanOptions

Equations

source

instance Lean.instToJsonLeanOptions :

ToJson LeanOptions

Equations