- 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
Equations
- Lean.instInhabitedDataValue = { default := Lean.DataValue.ofString default }
Equations
- Lean.instBEqDataValue = { beq := [anonymous] }
Equations
- Lean.instReprDataValue = { reprPrec := [anonymous] }
Equations
- Lean.DataValue.beqExp a b = (a == b)
Equations
Equations
- Lean.DataValue.getBoolEx x = match x with | Lean.DataValue.ofBool b => b | x => false
Equations
- Lean.DataValue.sameCtor x x = match x, x with | Lean.DataValue.ofString x, Lean.DataValue.ofString x_1 => true | Lean.DataValue.ofBool x, Lean.DataValue.ofBool x_1 => true | Lean.DataValue.ofName x, Lean.DataValue.ofName x_1 => true | Lean.DataValue.ofNat x, Lean.DataValue.ofNat x_1 => true | Lean.DataValue.ofInt x, Lean.DataValue.ofInt x_1 => true | Lean.DataValue.ofSyntax x, Lean.DataValue.ofSyntax x_1 => true | x, x_1 => false
Equations
- Lean.DataValue.str x = match x with | Lean.DataValue.ofString v => v | Lean.DataValue.ofBool v => toString v | Lean.DataValue.ofName v => toString v | Lean.DataValue.ofNat v => toString v | Lean.DataValue.ofInt v => toString v | Lean.DataValue.ofSyntax v => toString v
Equations
- Lean.instToStringDataValue = { toString := Lean.DataValue.str }
Equations
- Lean.instCoeStringDataValue = { coe := Lean.DataValue.ofString }
Equations
- Lean.instCoeBoolDataValue = { coe := Lean.DataValue.ofBool }
Equations
- Lean.instCoeNameDataValue = { coe := Lean.DataValue.ofName }
Equations
- Lean.instCoeNatDataValue = { coe := Lean.DataValue.ofNat }
Equations
- Lean.instCoeIntDataValue = { coe := Lean.DataValue.ofInt }
Equations
- Lean.instCoeSyntaxDataValue = { coe := Lean.DataValue.ofSyntax }
Equations
- Lean.instReprKVMap = { reprPrec := [anonymous] }
Equations
- Lean.instInhabitedKVMap = { default := { entries := default } }
Equations
- Lean.KVMap.instToStringKVMap = { toString := fun m => toString m.entries }
Equations
- Lean.KVMap.isEmpty x = match x with | { entries := m } => List.isEmpty m
Equations
- Lean.KVMap.size m = List.length m.entries
Equations
- Lean.KVMap.findCore [] x = none
- Lean.KVMap.findCore ((k, v) :: m) x = if (k == x) = true then some v else Lean.KVMap.findCore m x
Equations
- Lean.KVMap.find x x = match x, x with | { entries := m }, k => Lean.KVMap.findCore m k
Equations
- Lean.KVMap.findD m k d₀ = Option.getD (Lean.KVMap.find m k) d₀
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
Equations
- Lean.KVMap.insert x x x = match x, x, x with | { entries := m }, k, v => { entries := Lean.KVMap.insertCore m k v }
Equations
- Lean.KVMap.contains m n = Option.isSome (Lean.KVMap.find m n)
Equations
- Lean.KVMap.getString m k defVal = match Lean.KVMap.find m k with | some (Lean.DataValue.ofString v) => v | x => defVal
Equations
- Lean.KVMap.getNat m k defVal = match Lean.KVMap.find m k with | some (Lean.DataValue.ofNat v) => v | x => defVal
Equations
- Lean.KVMap.getInt m k defVal = match Lean.KVMap.find m k with | some (Lean.DataValue.ofInt v) => v | x => defVal
Equations
- Lean.KVMap.getBool m k defVal = match Lean.KVMap.find m k with | some (Lean.DataValue.ofBool v) => v | x => defVal
def
Lean.KVMap.getName
(m : Lean.KVMap)
(k : Lean.Name)
(defVal : optParam Lean.Name Lean.Name.anonymous)
:
Equations
- Lean.KVMap.getName m k defVal = match Lean.KVMap.find m k with | some (Lean.DataValue.ofName v) => v | x => defVal
def
Lean.KVMap.getSyntax
(m : Lean.KVMap)
(k : Lean.Name)
(defVal : optParam Lean.Syntax Lean.Syntax.missing)
:
Equations
- Lean.KVMap.getSyntax m k defVal = match Lean.KVMap.find m k with | some (Lean.DataValue.ofSyntax v) => v | x => defVal
Equations
- Lean.KVMap.setString m k v = Lean.KVMap.insert m k (Lean.DataValue.ofString v)
Equations
- Lean.KVMap.setNat m k v = Lean.KVMap.insert m k (Lean.DataValue.ofNat v)
Equations
- Lean.KVMap.setInt m k v = Lean.KVMap.insert m k (Lean.DataValue.ofInt v)
Equations
- Lean.KVMap.setBool m k v = Lean.KVMap.insert m k (Lean.DataValue.ofBool v)
Equations
- Lean.KVMap.setName m k v = Lean.KVMap.insert m k (Lean.DataValue.ofName v)
Equations
- Lean.KVMap.setSyntax m k v = Lean.KVMap.insert m k (Lean.DataValue.ofSyntax v)
@[inline]
def
Lean.KVMap.forIn
{δ : Type w}
{m : Type w → Type w'}
[inst : Monad m]
(kv : Lean.KVMap)
(init : δ)
(f : Lean.Name × Lean.DataValue → δ → m (ForInStep δ))
:
m δ
Equations
- Lean.KVMap.forIn kv init f = List.forIn kv.entries init f
Equations
- Lean.KVMap.subsetAux [] x = true
- Lean.KVMap.subsetAux ((k, v₁) :: m₁) x = match Lean.KVMap.find x k with | some v₂ => v₁ == v₂ && Lean.KVMap.subsetAux m₁ x | none => false
Equations
- Lean.KVMap.subset x x = match x, x with | { entries := m₁ }, m₂ => Lean.KVMap.subsetAux m₁ m₂
Equations
- Lean.KVMap.eqv m₁ m₂ = (Lean.KVMap.subset m₁ m₂ && Lean.KVMap.subset m₂ m₁)
Equations
- Lean.KVMap.instBEqKVMap = { beq := Lean.KVMap.eqv }
- toDataValue : α → Lean.DataValue
- ofDataValue? : Lean.DataValue → Option α
@[inline]
Equations
- Lean.KVMap.get? m k = Option.bind (Lean.KVMap.find m k) Lean.KVMap.Value.ofDataValue?
@[inline]
def
Lean.KVMap.get
{α : Type}
[s : Lean.KVMap.Value α]
(m : Lean.KVMap)
(k : Lean.Name)
(defVal : α)
:
α
Equations
- Lean.KVMap.get m k defVal = Option.getD (Lean.KVMap.get? m k) defVal
@[inline]
Equations
- Lean.KVMap.set m k v = Lean.KVMap.insert m k (Lean.KVMap.Value.toDataValue v)
Equations
- Lean.KVMap.instValueDataValue = { toDataValue := id, ofDataValue? := some }
Equations
- Lean.KVMap.instValueBool = { toDataValue := Lean.DataValue.ofBool, ofDataValue? := fun x => match x with | Lean.DataValue.ofBool b => some b | x => none }
Equations
- Lean.KVMap.instValueNat = { toDataValue := Lean.DataValue.ofNat, ofDataValue? := fun x => match x with | Lean.DataValue.ofNat n => some n | x => none }
Equations
- Lean.KVMap.instValueInt = { toDataValue := Lean.DataValue.ofInt, ofDataValue? := fun x => match x with | Lean.DataValue.ofInt i => some i | x => none }
Equations
- Lean.KVMap.instValueName = { toDataValue := Lean.DataValue.ofName, ofDataValue? := fun x => match x with | Lean.DataValue.ofName n => some n | x => none }
Equations
- Lean.KVMap.instValueString = { toDataValue := Lean.DataValue.ofString, ofDataValue? := fun x => match x with | Lean.DataValue.ofString n => some n | x => none }
Equations
- Lean.KVMap.instValueSyntax = { toDataValue := Lean.DataValue.ofSyntax, ofDataValue? := fun x => match x with | Lean.DataValue.ofSyntax n => some n | x => none }