Documentation

Lean.Compiler.LCNF.AlphaEqv

Alpha equivalence for LCNF Code

source
@[inline, reducible]
abbrev Lean.Compiler.LCNF.AlphaEqv.EqvM (α : Type) :
Type
Instances For
    source
    def Lean.Compiler.LCNF.AlphaEqv.eqvFVar (fvarId₁ : Lean.FVarId) (fvarId₂ : Lean.FVarId) :
    Lean.Compiler.LCNF.AlphaEqv.EqvM Bool
    Instances For
      source
      def Lean.Compiler.LCNF.AlphaEqv.eqvType (e₁ : Lean.Expr) (e₂ : Lean.Expr) :
      Lean.Compiler.LCNF.AlphaEqv.EqvM Bool
      Instances For
        source
        def Lean.Compiler.LCNF.AlphaEqv.eqvTypes (es₁ : Array Lean.Expr) (es₂ : Array Lean.Expr) :
        Lean.Compiler.LCNF.AlphaEqv.EqvM Bool
        Instances For
          source
          def Lean.Compiler.LCNF.AlphaEqv.eqvArg (a₁ : Lean.Compiler.LCNF.Arg) (a₂ : Lean.Compiler.LCNF.Arg) :
          Lean.Compiler.LCNF.AlphaEqv.EqvM Bool
          Instances For
            source
            def Lean.Compiler.LCNF.AlphaEqv.eqvArgs (as₁ : Array Lean.Compiler.LCNF.Arg) (as₂ : Array Lean.Compiler.LCNF.Arg) :
            Lean.Compiler.LCNF.AlphaEqv.EqvM Bool
            Instances For
              source
              def Lean.Compiler.LCNF.AlphaEqv.eqvLetValue (e₁ : Lean.Compiler.LCNF.LetValue) (e₂ : Lean.Compiler.LCNF.LetValue) :
              Lean.Compiler.LCNF.AlphaEqv.EqvM Bool
              Instances For
                source
                @[inline]
                def Lean.Compiler.LCNF.AlphaEqv.withFVar {α : Type} (fvarId₁ : Lean.FVarId) (fvarId₂ : Lean.FVarId) (x : Lean.Compiler.LCNF.AlphaEqv.EqvM α) :
                Lean.Compiler.LCNF.AlphaEqv.EqvM α
                Instances For
                  source
                  @[inline]
                  def Lean.Compiler.LCNF.AlphaEqv.withParams (params₁ : Array Lean.Compiler.LCNF.Param) (params₂ : Array Lean.Compiler.LCNF.Param) (x : Lean.Compiler.LCNF.AlphaEqv.EqvM Bool) :
                  Lean.Compiler.LCNF.AlphaEqv.EqvM Bool
                  Instances For
                    source
                    @[specialize #[]]
                    def Lean.Compiler.LCNF.AlphaEqv.withParams.go (params₁ : Array Lean.Compiler.LCNF.Param) (params₂ : Array Lean.Compiler.LCNF.Param) (x : Lean.Compiler.LCNF.AlphaEqv.EqvM Bool) (h : Array.size params₂ = Array.size params₁) (i : Nat) :
                    Lean.Compiler.LCNF.AlphaEqv.EqvM Bool
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Lean.Compiler.LCNF.AlphaEqv.sortAlts (alts : Array Lean.Compiler.LCNF.Alt) :
                      Array Lean.Compiler.LCNF.Alt
                      Instances For
                        source
                        partial def Lean.Compiler.LCNF.AlphaEqv.eqvAlts (alts₁ : Array Lean.Compiler.LCNF.Alt) (alts₂ : Array Lean.Compiler.LCNF.Alt) :
                        Lean.Compiler.LCNF.AlphaEqv.EqvM Bool
                        source
                        partial def Lean.Compiler.LCNF.AlphaEqv.eqv (code₁ : Lean.Compiler.LCNF.Code) (code₂ : Lean.Compiler.LCNF.Code) :
                        Lean.Compiler.LCNF.AlphaEqv.EqvM Bool
                        source
                        def Lean.Compiler.LCNF.Code.alphaEqv (c₁ : Lean.Compiler.LCNF.Code) (c₂ : Lean.Compiler.LCNF.Code) :
                        Bool

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

                        Instances For