inductive Lean.DataValue : Type

Value stored in a key-value map.

• ofString (v : String) : DataValue
• ofBool (v : Bool) : DataValue
• ofName (v : Name) : DataValue
• ofNat (v : Nat) : DataValue
• ofInt (v : Int) : DataValue
• ofSyntax (v : Syntax) : DataValue

instance Lean.instInhabitedDataValue : Inhabited DataValue

instance Lean.instBEqDataValue : BEq DataValue

instance Lean.instReprDataValue : Repr DataValue

@[export lean_data_value_beq]

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

@[export lean_mk_bool_data_value]

def Lean.mkBoolDataValueEx (b : Bool) : DataValue

@[export lean_data_value_bool]

def Lean.DataValue.getBoolEx : DataValue → Bool

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

@[export lean_data_value_to_string]

def Lean.DataValue.str : DataValue → String

instance Lean.instToStringDataValue : ToString DataValue

instance Lean.instCoeStringDataValue : Coe String DataValue

instance Lean.instCoeBoolDataValue : Coe Bool DataValue

instance Lean.instCoeNameDataValue : Coe Name DataValue

instance Lean.instCoeNatDataValue : Coe Nat DataValue

instance Lean.instCoeIntDataValue : Coe Int DataValue

instance Lean.instCoeSyntaxDataValue : Coe Syntax 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 (Name × DataValue)

instance Lean.instInhabitedKVMap : Inhabited KVMap

instance Lean.instReprKVMap : Repr KVMap

instance Lean.KVMap.instToString : ToString KVMap

def Lean.KVMap.empty : KVMap

def Lean.KVMap.isEmpty : KVMap → Bool

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

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

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

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

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

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

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

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

Erase an entry from the map

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

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

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

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

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

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

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

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

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

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

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

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

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

Update a String entry based on its current value.

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

Update a Nat entry based on its current value.

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

Update an Int entry based on its current value.

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

Update a Bool entry based on its current value.

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

Update a Name entry based on its current value.

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

Update a Syntax entry based on its current value.

@[inline]

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

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

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

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

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

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

instance Lean.KVMap.instBEq : BEq KVMap

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

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

instance Lean.KVMap.instValueDataValue : Value DataValue

instance Lean.KVMap.instValueBool : Value Bool

instance Lean.KVMap.instValueNat : Value Nat

instance Lean.KVMap.instValueInt : Value Int

instance Lean.KVMap.instValueName : Value Name

instance Lean.KVMap.instValueString : Value String

instance Lean.KVMap.instValueSyntax : Value Syntax