Documentation

Lean.Data.KVMap

inductive Lean.DataValue:
Type
@[export lean_data_value_beq]
Equations
@[export lean_mk_bool_data_value]
Equations
@[export lean_data_value_bool]
Equations
Equations
  • One or more equations did not get rendered due to their size.
@[export lean_data_value_to_string]
Equations
  • One or more equations did not get rendered due to their size.
structure Lean.KVMap:
Type
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
def Lean.KVMap.getNat (m : Lean.KVMap) (k : Lean.Name) (defVal : optParam Nat 0) :
Equations
def Lean.KVMap.getInt (m : Lean.KVMap) (k : Lean.Name) (defVal : optParam Int 0) :
Equations
Equations
Equations
@[inline]
def Lean.KVMap.forIn {δ : Type w} {m : Type wType w'} [inst : Monad m] (kv : Lean.KVMap) (init : δ) (f : Lean.Name × Lean.DataValueδm (ForInStep δ)) :
m δ
Equations
Equations
  • Lean.KVMap.instForInKVMapProdNameDataValue = { forIn := fun {β} [Monad m] => Lean.KVMap.forIn }
Equations
Equations
def Lean.KVMap.eqv (m₁ : Lean.KVMap) (m₂ : Lean.KVMap) :
Equations
@[inline]
def Lean.KVMap.get? {α : Type} [inst : Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) :
Equations
@[inline]
def Lean.KVMap.get {α : Type} [inst : Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) (defVal : α) :
α
Equations
@[inline]
def Lean.KVMap.set {α : Type} [inst : Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) (v : α) :
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations