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] [MonadEnv M] [MonadError M] (ext : NameMapExtension α) (k : Name) (v : α) :

          Add the given k,v pair to the NameMapExtension.

          Equations
            Instances For
              def Lean.registerNameMapExtension (α : Type) (name : Name := by exact decl_name%) :

              Registers a new extension with the given name and type.

              Equations
                Instances For

                  The inputs to registerNameMapAttribute.

                  • name : Name

                    The name of the attribute

                  • ref : Name

                    The declaration which creates the attribute

                  • descr : String

                    The description of the attribute

                  • add (src : Name) (stx : Syntax) : AttrM α

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

                  Instances For

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

                    Equations
                      Instances For