Documentation

Lean.Compiler.IR.NormIds

@[reducible, inline]
Equations
    Instances For
      Equations
        Instances For
          Equations
            Instances For
              Equations
                Instances For

                  Return true if variable, parameter and join point ids are unique

                  Equations
                    Instances For
                      @[reducible, inline]
                      Equations
                        Instances For
                          Equations
                            Instances For
                              Equations
                                Instances For
                                  Equations
                                    Instances For
                                      Equations
                                        Instances For
                                          Equations
                                            Instances For
                                              @[reducible, inline]
                                              Equations
                                                Instances For
                                                  @[inline]
                                                  def Lean.IR.NormalizeIds.withVar {α : Type} (x : VarId) (k : VarIdN α) :
                                                  N α
                                                  Equations
                                                    Instances For
                                                      @[inline]
                                                      def Lean.IR.NormalizeIds.withJP {α : Type} (x : JoinPointId) (k : JoinPointIdN α) :
                                                      N α
                                                      Equations
                                                        Instances For
                                                          @[inline]
                                                          def Lean.IR.NormalizeIds.withParams {α : Type} (ps : Array Param) (k : Array ParamN α) :
                                                          N α
                                                          Equations
                                                            Instances For
                                                              Equations
                                                                Instances For

                                                                  Create a declaration equivalent to d s.t. d.normalizeIds.uniqueIds == true

                                                                  Equations
                                                                    Instances For

                                                                      Apply a function f : VarId → VarId to variable occurrences. The following functions assume the IR code does not have variable shadowing.

                                                                      @[inline]
                                                                      Equations
                                                                        Instances For
                                                                          Equations
                                                                            Instances For
                                                                              Equations
                                                                                Instances For
                                                                                  @[inline]
                                                                                  Equations
                                                                                    Instances For

                                                                                      Replace x with y in b. This function assumes b does not shadow x

                                                                                      Equations
                                                                                        Instances For