inductive Lean.DataValue : Type

Value stored in a key-value map.

• ofString: String → Lean.DataValue
• ofBool: Bool → Lean.DataValue
• ofName: Lean.Name → Lean.DataValue
• ofNat: Nat → Lean.DataValue
• ofInt: Int → Lean.DataValue
• ofSyntax: Lean.Syntax → Lean.DataValue

instance Lean.instInhabitedDataValue : Inhabited Lean.DataValue

Equations

• Lean.instInhabitedDataValue = { default := Lean.DataValue.ofString default }

instance Lean.instBEqDataValue : BEq Lean.DataValue

instance Lean.instReprDataValue : Repr Lean.DataValue

@[export lean_data_value_beq]

def Lean.DataValue.beqExp (a b : Lean.DataValue) : Bool

Equations

• a.beqExp b = (a == b)

@[export lean_mk_bool_data_value]

def Lean.mkBoolDataValueEx (b : Bool) : Lean.DataValue

@[export lean_data_value_bool]

def Lean.DataValue.getBoolEx : Lean.DataValue → Bool

Equations

• (Lean.DataValue.ofBool b).getBoolEx = b
• x.getBoolEx = false

def Lean.DataValue.sameCtor : Lean.DataValue → Lean.DataValue → Bool

Equations

• (Lean.DataValue.ofString a).sameCtor (Lean.DataValue.ofString b) = true
• (Lean.DataValue.ofBool a).sameCtor (Lean.DataValue.ofBool b) = true
• (Lean.DataValue.ofName a).sameCtor (Lean.DataValue.ofName b) = true
• (Lean.DataValue.ofNat a).sameCtor (Lean.DataValue.ofNat b) = true
• (Lean.DataValue.ofInt a).sameCtor (Lean.DataValue.ofInt b) = true
• (Lean.DataValue.ofSyntax a).sameCtor (Lean.DataValue.ofSyntax b) = true
• x✝.sameCtor x = false

@[export lean_data_value_to_string]

def Lean.DataValue.str : Lean.DataValue → String

Equations

• (Lean.DataValue.ofString a).str = a
• (Lean.DataValue.ofBool a).str = toString a
• (Lean.DataValue.ofName a).str = toString a
• (Lean.DataValue.ofNat a).str = toString a
• (Lean.DataValue.ofInt a).str = toString a
• (Lean.DataValue.ofSyntax a).str = toString a

instance Lean.instToStringDataValue : ToString Lean.DataValue

Equations

• Lean.instToStringDataValue = { toString := Lean.DataValue.str }

instance Lean.instCoeStringDataValue : Coe String Lean.DataValue

instance Lean.instCoeBoolDataValue : Coe Bool Lean.DataValue

Equations

• Lean.instCoeBoolDataValue = { coe := Lean.DataValue.ofBool }

instance Lean.instCoeNameDataValue : Coe Lean.Name Lean.DataValue

instance Lean.instCoeNatDataValue : Coe Nat Lean.DataValue

Equations

• Lean.instCoeNatDataValue = { coe := Lean.DataValue.ofNat }

instance Lean.instCoeIntDataValue : Coe Int Lean.DataValue

instance Lean.instCoeSyntaxDataValue : Coe Lean.Syntax Lean.DataValue

structure Lean.KVMap : Type

A key-value map. We use it to represent user-selected options and Expr.mdata.

Remark: we do not use RBMap here because we need to manipulate KVMap objects in C++ and RBMap is implemented in Lean. So, we use just a List until we can generate C++ code from Lean code.

• entries : List (Lean.Name × Lean.DataValue)

instance Lean.instInhabitedKVMap : Inhabited Lean.KVMap

Equations

• Lean.instInhabitedKVMap = { default := { entries := default } }

instance Lean.instReprKVMap : Repr Lean.KVMap

instance Lean.KVMap.instToString : ToString Lean.KVMap

Equations

• Lean.KVMap.instToString = { toString := fun (m : Lean.KVMap) => toString m.entries }

def Lean.KVMap.empty : Lean.KVMap

def Lean.KVMap.isEmpty : Lean.KVMap → Bool

Equations

• { entries := m }.isEmpty = m.isEmpty

def Lean.KVMap.size (m : Lean.KVMap) : Nat

def Lean.KVMap.findCore : List (Lean.Name × Lean.DataValue) → Lean.Name → Option Lean.DataValue

def Lean.KVMap.find : Lean.KVMap → Lean.Name → Option Lean.DataValue

def Lean.KVMap.findD (m : Lean.KVMap) (k : Lean.Name) (d₀ : Lean.DataValue) : Lean.DataValue

Equations

• m.findD k d₀ = (m.find k).getD d₀

def Lean.KVMap.insertCore : List (Lean.Name × Lean.DataValue) → Lean.Name → Lean.DataValue → List (Lean.Name × Lean.DataValue)

Equations

• Lean.KVMap.insertCore [] x✝ x = [(x✝, x)]
• Lean.KVMap.insertCore ((k, v) :: m) x✝ x = if (k == x✝) = true then (k, x) :: m else (k, v) :: Lean.KVMap.insertCore m x✝ x

def Lean.KVMap.insert : Lean.KVMap → Lean.Name → Lean.DataValue → Lean.KVMap

def Lean.KVMap.contains (m : Lean.KVMap) (n : Lean.Name) : Bool

def Lean.KVMap.erase : Lean.KVMap → Lean.Name → Lean.KVMap

Erase an entry from the map

Equations

• { entries := m }.erase x = { entries := List.filter (fun (a : Lean.Name × Lean.DataValue) => decide (a.fst ≠ x)) m }

def Lean.KVMap.getString (m : Lean.KVMap) (k : Lean.Name) (defVal : String := "") : String

def Lean.KVMap.getNat (m : Lean.KVMap) (k : Lean.Name) (defVal : Nat := 0) : Nat

Equations

• m.getNat k defVal = match m.find k with | some (Lean.DataValue.ofNat v) => v | x => defVal

def Lean.KVMap.getInt (m : Lean.KVMap) (k : Lean.Name) (defVal : Int := 0) : Int

def Lean.KVMap.getBool (m : Lean.KVMap) (k : Lean.Name) (defVal : Bool := false) : Bool

Equations

• m.getBool k defVal = match m.find k with | some (Lean.DataValue.ofBool v) => v | x => defVal

def Lean.KVMap.getName (m : Lean.KVMap) (k : Lean.Name) (defVal : Lean.Name := Lean.Name.anonymous) : Lean.Name

Equations

• m.getName k defVal = match m.find k with | some (Lean.DataValue.ofName v) => v | x => defVal

def Lean.KVMap.getSyntax (m : Lean.KVMap) (k : Lean.Name) (defVal : Lean.Syntax := Lean.Syntax.missing) : Lean.Syntax

def Lean.KVMap.setString (m : Lean.KVMap) (k : Lean.Name) (v : String) : Lean.KVMap

Equations

• m.setString k v = m.insert k (Lean.DataValue.ofString v)

def Lean.KVMap.setNat (m : Lean.KVMap) (k : Lean.Name) (v : Nat) : Lean.KVMap

def Lean.KVMap.setInt (m : Lean.KVMap) (k : Lean.Name) (v : Int) : Lean.KVMap

Equations

• m.setInt k v = m.insert k (Lean.DataValue.ofInt v)

def Lean.KVMap.setBool (m : Lean.KVMap) (k : Lean.Name) (v : Bool) : Lean.KVMap

def Lean.KVMap.setName (m : Lean.KVMap) (k v : Lean.Name) : Lean.KVMap

Equations

• m.setName k v = m.insert k (Lean.DataValue.ofName v)

def Lean.KVMap.setSyntax (m : Lean.KVMap) (k : Lean.Name) (v : Lean.Syntax) : Lean.KVMap

def Lean.KVMap.updateString (m : Lean.KVMap) (k : Lean.Name) (f : String → String) : Lean.KVMap

Update a String entry based on its current value.

Equations

• m.updateString k f = m.insert k (Lean.DataValue.ofString (f (m.getString k)))

def Lean.KVMap.updateNat (m : Lean.KVMap) (k : Lean.Name) (f : Nat → Nat) : Lean.KVMap

Update a Nat entry based on its current value.

def Lean.KVMap.updateInt (m : Lean.KVMap) (k : Lean.Name) (f : Int → Int) : Lean.KVMap

Update an Int entry based on its current value.

def Lean.KVMap.updateBool (m : Lean.KVMap) (k : Lean.Name) (f : Bool → Bool) : Lean.KVMap

Update a Bool entry based on its current value.

def Lean.KVMap.updateName (m : Lean.KVMap) (k : Lean.Name) (f : Lean.Name → Lean.Name) : Lean.KVMap

Update a Name entry based on its current value.

Equations

• m.updateName k f = m.insert k (Lean.DataValue.ofName (f (m.getName k)))

def Lean.KVMap.updateSyntax (m : Lean.KVMap) (k : Lean.Name) (f : Lean.Syntax → Lean.Syntax) : Lean.KVMap

Update a Syntax entry based on its current value.

Equations

• m.updateSyntax k f = m.insert k (Lean.DataValue.ofSyntax (f (m.getSyntax k)))

@[inline]

def Lean.KVMap.forIn {δ : Type w} {m : Type w → Type w'} [Monad m] (kv : Lean.KVMap) (init : δ) (f : Lean.Name × Lean.DataValue → δ → m (ForInStep δ)) : m δ

Equations

• kv.forIn init f = forIn kv.entries init f

instance Lean.KVMap.instForInProdNameDataValue {m : Type u_1 → Type u_2} : ForIn m Lean.KVMap (Lean.Name × Lean.DataValue)

Equations

• Lean.KVMap.instForInProdNameDataValue = { forIn := fun {β : Type ?u.14} [Monad m] => Lean.KVMap.forIn }

def Lean.KVMap.subsetAux : List (Lean.Name × Lean.DataValue) → Lean.KVMap → Bool

def Lean.KVMap.subset : Lean.KVMap → Lean.KVMap → Bool

def Lean.KVMap.mergeBy (mergeFn : Lean.Name → Lean.DataValue → Lean.DataValue → Lean.DataValue) (l r : Lean.KVMap) : Lean.KVMap

def Lean.KVMap.eqv (m₁ m₂ : Lean.KVMap) : Bool

Equations

• m₁.eqv m₂ = (m₁.subset m₂ && m₂.subset m₁)

instance Lean.KVMap.instBEq : BEq Lean.KVMap

class Lean.KVMap.Value (α : Type) : Type

• toDataValue : α → Lean.DataValue
• ofDataValue? : Lean.DataValue → Option α

@[inline]

def Lean.KVMap.get? {α : Type} [Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) : Option α

Equations

• m.get? k = (m.find k).bind Lean.KVMap.Value.ofDataValue?

@[inline]

def Lean.KVMap.get {α : Type} [Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) (defVal : α) : α

@[inline]

def Lean.KVMap.set {α : Type} [Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) (v : α) : Lean.KVMap

@[inline]

def Lean.KVMap.update {α : Type} [Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) (f : Option α → Option α) : Lean.KVMap

instance Lean.KVMap.instValueDataValue : Lean.KVMap.Value Lean.DataValue

instance Lean.KVMap.instValueBool : Lean.KVMap.Value Bool

Equations

• Lean.KVMap.instValueBool = { toDataValue := Lean.DataValue.ofBool, ofDataValue? := fun (x : Lean.DataValue) => match x with | Lean.DataValue.ofBool b => some b | x => none }

instance Lean.KVMap.instValueNat : Lean.KVMap.Value Nat

Equations

• Lean.KVMap.instValueNat = { toDataValue := Lean.DataValue.ofNat, ofDataValue? := fun (x : Lean.DataValue) => match x with | Lean.DataValue.ofNat n => some n | x => none }

instance Lean.KVMap.instValueInt : Lean.KVMap.Value Int

Equations

• Lean.KVMap.instValueInt = { toDataValue := Lean.DataValue.ofInt, ofDataValue? := fun (x : Lean.DataValue) => match x with | Lean.DataValue.ofInt i => some i | x => none }

instance Lean.KVMap.instValueName : Lean.KVMap.Value Lean.Name

Equations

• Lean.KVMap.instValueName = { toDataValue := Lean.DataValue.ofName, ofDataValue? := fun (x : Lean.DataValue) => match x with | Lean.DataValue.ofName n => some n | x => none }

instance Lean.KVMap.instValueString : Lean.KVMap.Value String

instance Lean.KVMap.instValueSyntax : Lean.KVMap.Value Lean.Syntax

Equations

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