Documentation

Lean.Compiler.LCNF.AlphaEqv

Alpha equivalence for LCNF Code

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

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

                                              Equations
                                                Instances For