Documentation

Lean.Compiler.LCNF.AuxDeclCache

source
structure Lean.Compiler.LCNF.AuxDeclCacheKey :
Type
Instances For
    source
    def Lean.Compiler.LCNF.instBEqAuxDeclCacheKey.beq :
    AuxDeclCacheKey → AuxDeclCacheKey → Bool
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Compiler.LCNF.instBEqAuxDeclCacheKey :
      BEq AuxDeclCacheKey
      source
      @[implicit_reducible]
      instance Lean.Compiler.LCNF.instHashableAuxDeclCacheKey :
      Hashable AuxDeclCacheKey
      source
      def Lean.Compiler.LCNF.instHashableAuxDeclCacheKey.hash :
      AuxDeclCacheKey → UInt64
      Instances For
        source
        opaque Lean.Compiler.LCNF.auxDeclCacheExt :
        CacheExtension AuxDeclCacheKey Name
        source
        inductive Lean.Compiler.LCNF.CacheAuxDeclResult :
        Type
        Instances For
          source
          def Lean.Compiler.LCNF.cacheAuxDecl {pu : Purity} (decl : Decl pu) :
          CompilerM CacheAuxDeclResult
          Instances For