Documentation

Lean.Data.KVMap

inductive Lean.DataValue :

Value stored in a key-value map.

Instances For
    @[export lean_data_value_beq]
    Equations
    • a.beqExp b = (a == b)
    Instances For
      @[export lean_mk_bool_data_value]
      Equations
      Instances For
        @[export lean_data_value_bool]
        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[export lean_data_value_to_string]
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              structure Lean.KVMap :

              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.

              Instances For
                Equations
                Equations
                Equations
                Instances For
                  Equations
                  • x.isEmpty = match x with | { entries := m } => m.isEmpty
                  Instances For
                    Equations
                    • m.size = m.entries.length
                    Instances For
                      Equations
                      Instances For
                        Equations
                        • m.findD k d₀ = (m.find k).getD d₀
                        Instances For
                          Equations
                          Instances For
                            Equations
                            • x✝¹.insert x✝ x = match x✝¹, x✝, x with | { entries := m }, k, v => { entries := Lean.KVMap.insertCore m k v }
                            Instances For
                              Equations
                              • m.contains n = (m.find n).isSome
                              Instances For

                                Erase an entry from the map

                                Equations
                                Instances For
                                  Equations
                                  Instances For
                                    def Lean.KVMap.getNat (m : Lean.KVMap) (k : Lake.Name) (defVal : optParam Nat 0) :
                                    Equations
                                    Instances For
                                      def Lean.KVMap.getInt (m : Lean.KVMap) (k : Lake.Name) (defVal : optParam Int 0) :
                                      Equations
                                      Instances For
                                        Equations
                                        Instances For
                                          Equations
                                          Instances For
                                            Equations
                                            Instances For
                                              Equations
                                              Instances For
                                                Equations
                                                Instances For
                                                  Equations
                                                  Instances For
                                                    Equations
                                                    Instances For
                                                      Equations
                                                      Instances For
                                                        Equations
                                                        Instances For

                                                          Update a String entry based on its current value.

                                                          Equations
                                                          Instances For

                                                            Update a Nat entry based on its current value.

                                                            Equations
                                                            Instances For

                                                              Update an Int entry based on its current value.

                                                              Equations
                                                              Instances For

                                                                Update a Bool entry based on its current value.

                                                                Equations
                                                                Instances For

                                                                  Update a Name entry based on its current value.

                                                                  Equations
                                                                  Instances For

                                                                    Update a Syntax entry based on its current value.

                                                                    Equations
                                                                    Instances For
                                                                      @[inline]
                                                                      def Lean.KVMap.forIn {δ : Type w} {m : Type w → Type w'} [Monad m] (kv : Lean.KVMap) (init : δ) (f : Lake.Name × Lean.DataValueδm (ForInStep δ)) :
                                                                      m δ
                                                                      Equations
                                                                      • kv.forIn init f = kv.entries.forIn init f
                                                                      Instances For
                                                                        Equations
                                                                        • Lean.KVMap.instForInProdNameDataValue = { forIn := fun {β : Type u_1} [Monad m] => Lean.KVMap.forIn }
                                                                        Equations
                                                                        Instances For
                                                                          Equations
                                                                          Instances For
                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              def Lean.KVMap.eqv (m₁ : Lean.KVMap) (m₂ : Lean.KVMap) :
                                                                              Equations
                                                                              • m₁.eqv m₂ = (m₁.subset m₂ && m₂.subset m₁)
                                                                              Instances For
                                                                                class Lean.KVMap.Value (α : Type) :
                                                                                Instances
                                                                                  @[inline]
                                                                                  Equations
                                                                                  • m.get? k = (m.find k).bind Lean.KVMap.Value.ofDataValue?
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    def Lean.KVMap.get {α : Type} [Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lake.Name) (defVal : α) :
                                                                                    α
                                                                                    Equations
                                                                                    • m.get k defVal = (m.get? k).getD defVal
                                                                                    Instances For
                                                                                      @[inline]
                                                                                      def Lean.KVMap.set {α : Type} [Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lake.Name) (v : α) :
                                                                                      Equations
                                                                                      Instances For
                                                                                        @[inline]
                                                                                        def Lean.KVMap.update {α : Type} [Lean.KVMap.Value α] (m : Lean.KVMap) (k : Lake.Name) (f : Option αOption α) :
                                                                                        Equations
                                                                                        • m.update k f = match f (m.get? k) with | some a => m.set k a | none => m.erase k
                                                                                        Instances For
                                                                                          Equations
                                                                                          Equations
                                                                                          Equations
                                                                                          Equations
                                                                                          Equations
                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.