Documentation

Lean.Meta.Tactic.Grind.VarRename

source
@[reducible, inline]
abbrev Lean.Meta.Grind.Var :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Lean.Meta.Grind.FoundVars :
    Type
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Meta.Grind.VarCollector :
      Type
      Instances For
        source
        def Lean.Meta.Grind.collectVar (x : Var) :
        VarCollector
        Instances For
          source
          @[implicit_reducible]
          instance Lean.Meta.Grind.instAndThenVarCollector :
          AndThen VarCollector
          source
          def Lean.Meta.Grind.collectMapVars {α : Type u_1} {Expr : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashMap α Expr) (k : α → VarCollector) :
          VarCollector
          Instances For
            source
            def Lean.Meta.Grind.FoundVars.toArray (s : FoundVars) :
            Array Var
            Instances For
              source
              structure Lean.Meta.Grind.VarRename :
              Type
              Instances For
                source
                @[implicit_reducible]
                instance Lean.Meta.Grind.instCoeFunVarRenameForallVar :
                CoeFun VarRename fun (x : VarRename) => Var → Var
                source
                def Lean.Meta.Grind.mkVarRename (new2old : Array Var) :
                VarRename
                Instances For