- 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] }
@[export lean_data_value_beq]
Equations
- Lean.DataValue.beqExp a b = (a == b)
@[export lean_mk_bool_data_value]
Equations
@[export lean_data_value_bool]
Equations
- Lean.DataValue.getBoolEx _fun_discr = match _fun_discr with | Lean.DataValue.ofBool b => b | x => false
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.
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.instInhabitedKVMap = { default := { entries := default } }
Equations
- Lean.instReprKVMap = { reprPrec := [anonymous] }
Equations
- Lean.KVMap.instToStringKVMap = { toString := fun m => toString m.entries }
Equations
- Lean.KVMap.isEmpty _fun_discr = match _fun_discr with | { entries := m } => List.isEmpty m
Equations
- Lean.KVMap.findCore [] _fun_discr = none
- Lean.KVMap.findCore ((k, v) :: m) _fun_discr = if (k == _fun_discr) = true then some v else Lean.KVMap.findCore m _fun_discr
Equations
- Lean.KVMap.find _fun_discr _fun_discr = match _fun_discr, _fun_discr 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 [] _fun_discr _fun_discr = [(_fun_discr, _fun_discr)]
- Lean.KVMap.insertCore ((k, v) :: m) _fun_discr _fun_discr = if (k == _fun_discr) = true then (k, _fun_discr) :: m else (k, v) :: Lean.KVMap.insertCore m _fun_discr _fun_discr
Equations
- Lean.KVMap.insert _fun_discr _fun_discr _fun_discr = match _fun_discr, _fun_discr, _fun_discr 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 [] _fun_discr = true
- Lean.KVMap.subsetAux ((k, v₁) :: m₁) _fun_discr = match Lean.KVMap.find _fun_discr k with | some v₂ => v₁ == v₂ && Lean.KVMap.subsetAux m₁ _fun_discr | none => false
Equations
- Lean.KVMap.subset _fun_discr _fun_discr = match _fun_discr, _fun_discr 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]
def
Lean.KVMap.get?
{α : Type}
[inst : Lean.KVMap.Value α]
(m : Lean.KVMap)
(k : Lean.Name)
:
Option α
Equations
- Lean.KVMap.get? m k = Option.bind (Lean.KVMap.find m k) Lean.KVMap.Value.ofDataValue?
@[inline]
def
Lean.KVMap.get
{α : Type}
[inst : 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]
def
Lean.KVMap.set
{α : Type}
[inst : Lean.KVMap.Value α]
(m : Lean.KVMap)
(k : Lean.Name)
(v : α)
:
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 }