Documentation

Lean.Data.KVMap

inductive Lean.DataValue :
Type
Equations
structure Lean.KVMap :
Type
Equations
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} [s : Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) :
Equations
@[inline]
def Lean.KVMap.get {α : Type} [s : Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) (defVal : α) :
α
Equations
@[inline]
def Lean.KVMap.set {α : Type} [s : Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lean.Name) (v : α) :
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations