Documentation

Lean.Compiler.LCNF.DeclHash

source
@[implicit_reducible]
instance Lean.Compiler.LCNF.instHashableParam {pu : Purity} :
Hashable (Param pu)
source
def Lean.Compiler.LCNF.hashParams {pu : Purity} (ps : Array (Param pu)) :
UInt64
Instances For
    source
    partial def Lean.Compiler.LCNF.hashAlt {pu : Purity} (alt : Alt pu) :
    UInt64
    source
    partial def Lean.Compiler.LCNF.hashAlts {pu : Purity} (alts : Array (Alt pu)) :
    UInt64
    source
    partial def Lean.Compiler.LCNF.hashCode {pu : Purity} (code : Code pu) :
    UInt64
    source
    @[implicit_reducible]
    instance Lean.Compiler.LCNF.instHashableCode {pu : Purity} :
    Hashable (Code pu)
    source
    def Lean.Compiler.LCNF.instHashableDeclValue.hash {pu✝ : Purity} :
    DeclValue pu✝ → UInt64
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Compiler.LCNF.instHashableDeclValue {pu✝ : Purity} :
      Hashable (DeclValue pu✝)
      source
      def Lean.Compiler.LCNF.instHashableSignature.hash {pu✝ : Purity} :
      Signature pu✝ → UInt64
      Instances For
        source
        @[implicit_reducible]
        instance Lean.Compiler.LCNF.instHashableSignature {pu✝ : Purity} :
        Hashable (Signature pu✝)
        source
        @[implicit_reducible]
        instance Lean.Compiler.LCNF.instHashableDecl {pu✝ : Purity} :
        Hashable (Decl pu✝)
        source
        def Lean.Compiler.LCNF.instHashableDecl.hash {pu✝ : Purity} :
        Decl pu✝ → UInt64
        Instances For