Documentation

Lean.Compiler.LCNF.AlphaEqv

Alpha equivalence for LCNF Code

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.AlphaEqv.EqvM (α : Type) :
Type
Instances For
    source
    def Lean.Compiler.LCNF.AlphaEqv.eqvFVar (fvarId₁ fvarId₂ : FVarId) :
    EqvM Bool
    Instances For
      source
      def Lean.Compiler.LCNF.AlphaEqv.eqvType (e₁ e₂ : Expr) :
      EqvM Bool
      Instances For
        source
        def Lean.Compiler.LCNF.AlphaEqv.eqvTypes (es₁ es₂ : Array Expr) :
        EqvM Bool
        Instances For
          source
          def Lean.Compiler.LCNF.AlphaEqv.eqvArg {pu : Purity} (a₁ a₂ : Arg pu) :
          EqvM Bool
          Instances For
            source
            def Lean.Compiler.LCNF.AlphaEqv.eqvArgs {pu : Purity} (as₁ as₂ : Array (Arg pu)) :
            EqvM Bool
            Instances For
              source
              def Lean.Compiler.LCNF.AlphaEqv.eqvLetValue {pu : Purity} (e₁ e₂ : LetValue pu) :
              EqvM Bool
              Instances For
                source
                @[inline]
                def Lean.Compiler.LCNF.AlphaEqv.withFVar {α : Type} (fvarId₁ fvarId₂ : FVarId) (x : EqvM α) :
                EqvM α
                Instances For
                  source
                  @[inline]
                  def Lean.Compiler.LCNF.AlphaEqv.withParams {pu : Purity} (params₁ params₂ : Array (Param pu)) (x : EqvM Bool) :
                  EqvM Bool
                  Instances For
                    source
                    def Lean.Compiler.LCNF.AlphaEqv.sortAlts {pu : Purity} (alts : Array (Alt pu)) :
                    Array (Alt pu)
                    Instances For
                      source
                      partial def Lean.Compiler.LCNF.AlphaEqv.eqvAlts {pu : Purity} (alts₁ alts₂ : Array (Alt pu)) :
                      EqvM Bool
                      source
                      partial def Lean.Compiler.LCNF.AlphaEqv.eqv {pu : Purity} (code₁ code₂ : Code pu) :
                      EqvM Bool
                      source
                      def Lean.Compiler.LCNF.Code.alphaEqv {pu : Purity} (c₁ c₂ : Code pu) :
                      Bool

                      Return true if c₁ and c₂ are alpha equivalent.

                      Instances For