Documentation

Lean.Meta.CoeAttr

The @[coe] attribute, used to delaborate coercion functions as ↑ #

When writing a coercion, if the pattern

@[coe]
def A.toB (a : A) : B := sorry

instance : Coe A B where coe := A.toB

is used, then A.toB a will be pretty-printed as ↑a.

source
inductive Lean.Meta.CoeFnType :
Type

The different types of coercions that are supported by the coe attribute.

Instances For
    source
    def Lean.Meta.instInhabitedCoeFnType.default :
    CoeFnType
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Meta.instInhabitedCoeFnType :
      Inhabited CoeFnType
      source
      @[implicit_reducible]
      instance Lean.Meta.instReprCoeFnType :
      Repr CoeFnType
      source
      def Lean.Meta.instReprCoeFnType.repr :
      CoeFnType → Nat → Format
      Instances For
        source
        @[implicit_reducible]
        instance Lean.Meta.instDecidableEqCoeFnType :
        DecidableEq CoeFnType
        source
        @[implicit_reducible]
        instance Lean.Meta.instToExprCoeFnType :
        ToExpr CoeFnType
        source
        structure Lean.Meta.CoeFnInfo :
        Type

        Information associated to a coercion function to enable sensible delaboration.

        • numArgs : Nat

          The number of arguments to the coercion function

        • coercee : Nat

          The argument index that represents the value being coerced

        • type : CoeFnType

          The type of coercion

        Instances For
          source
          @[implicit_reducible]
          instance Lean.Meta.instInhabitedCoeFnInfo :
          Inhabited CoeFnInfo
          source
          def Lean.Meta.instInhabitedCoeFnInfo.default :
          CoeFnInfo
          Instances For
            source
            @[implicit_reducible]
            instance Lean.Meta.instReprCoeFnInfo :
            Repr CoeFnInfo
            source
            def Lean.Meta.instReprCoeFnInfo.repr :
            CoeFnInfo → Nat → Format
            Instances For
              source
              @[implicit_reducible]
              instance Lean.Meta.instToExprCoeFnInfo :
              ToExpr CoeFnInfo
              source
              opaque Lean.Meta.coeExt :
              SimpleScopedEnvExtension (Name × CoeFnInfo) (NameMap CoeFnInfo)

              The environment extension for tracking coercion functions for delaboration

              source
              def Lean.Meta.getCoeFnInfo? (fn : Name) :
              CoreM (Option CoeFnInfo)

              Lookup the coercion information for a given function

              Instances For
                source
                def Lean.Meta.registerCoercion (name : Name) (info : Option CoeFnInfo := none) :
                MetaM Unit

                Add name to the coercion extension and add a coercion delaborator for the function.

                Instances For