Documentation

Batteries.Lean.NameMapAttribute

Maps declaration names to α.

Equations
Instances For

    Look up a value in the given extension in the environment.

    Equations
    Instances For
      def Lean.NameMapExtension.add {M : TypeType} {α : Type} [Monad M] [Lean.MonadEnv M] [Lean.MonadError M] (ext : Lean.NameMapExtension α) (k : Lean.Name) (v : α) :

      Add the given k,v pair to the NameMapExtension.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Registers a new extension with the given name and type.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The inputs to registerNameMapAttribute.

          • name : Lean.Name

            The name of the attribute

          • ref : Lean.Name

            The declaration which creates the attribute

          • descr : String

            The description of the attribute

          • This function is called when the attribute is applied. It should produce a value of type α from the given attribute syntax.

          Instances For
            Equations
            • Lean.instInhabitedNameMapAttributeImpl = { default := { name := default, ref := default, descr := default, add := default } }

            Similar to registerParametricAttribute except that attributes do not have to be assigned in the same file as the declaration.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For