Documentation

Lean.Compiler.ImplementedByAttr

source
opaque Lean.Compiler.implementedByAttr :
ParametricAttribute Name

Instructs the compiler to use a different function as the implementation of a function. With the exception of tactics that call native code such as native_decide, the kernel and type checking are unaffected. When this attribute is used on a function, the function is not compiled and all compiler-related attributes (e.g. noncomputable, @[inline]) are ignored. Calls to this function are replaced by calls to its implementation.

The most common use cases of @[implemented_by] are to provide an efficient unsafe implementation and to make an unsafe function accessible in safe code through an opaque function:

unsafe def testEqImpl (as bs : Array Nat) : Bool :=
  ptrEq as bs || as == bs

@[implemented_by testEqImpl]
def testEq (as bs : Array Nat) : Bool :=
  as == bs

unsafe def printAddrImpl {α : Type u} (x : α) : IO Unit :=
  IO.println s!"Address: {ptrAddrUnsafe x}"

@[implemented_by printAddrImpl]
opaque printAddr {α : Type u} (x : α) : IO Unit

The provided implementation is not checked to be equivalent to the original definition. This makes it possible to prove False with native_decide using incorrect implementations. For a safer variant of this attribute that however doesn't work for unsafe implementations, see @[csimp], which requires a proof that the two functions are equal.

source
@[export lean_get_implemented_by]
def Lean.Compiler.getImplementedBy? (env : Environment) (declName : Name) :
Option Name
Equations
Instances For
    source
    def Lean.Compiler.setImplementedBy (env : Environment) (declName impName : Name) :
    Except String Environment
    Equations
    Instances For
      source
      def Lean.setImplementedBy {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (declName impName : Name) :
      m Unit
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For