inductive Lean.Elab.Tactic.Do.Uses : Type

• zero : Uses
• one : Uses
• many : Uses

instance Lean.Elab.Tactic.Do.instBEqUses : BEq Uses

def Lean.Elab.Tactic.Do.instBEqUses.beq : Uses → Uses → Bool

def Lean.Elab.Tactic.Do.instOrdUses.ord : Uses → Uses → Ordering

instance Lean.Elab.Tactic.Do.instOrdUses : Ord Uses

instance Lean.Elab.Tactic.Do.instInhabitedUses : Inhabited Uses

def Lean.Elab.Tactic.Do.instInhabitedUses.default : Uses

def Lean.Elab.Tactic.Do.Uses.add : Uses → Uses → Uses

def Lean.Elab.Tactic.Do.Uses.toNat : Uses → Nat

def Lean.Elab.Tactic.Do.Uses.fromNat : Nat → Uses

instance Lean.Elab.Tactic.Do.instAddUses : Add Uses

@[reducible, inline]

abbrev Lean.Elab.Tactic.Do.FVarUses : Type

def Lean.Elab.Tactic.Do.FVarUses.add (a b : FVarUses) : FVarUses

instance Lean.Elab.Tactic.Do.instAddFVarUses : Add FVarUses

inductive Lean.Elab.Tactic.Do.BVarUses (n : Nat) : Type

• none {n : Nat} : BVarUses n
• some {n : Nat} (uses : Vector Uses n) : BVarUses n

def Lean.Elab.Tactic.Do.BVarUses.single {numBVars : Nat} (n : Nat) : autoParam (n < numBVars) single._auto_1 → BVarUses numBVars

def Lean.Elab.Tactic.Do.BVarUses.pop {numBVars : Nat} : BVarUses (numBVars + 1) → Uses × BVarUses numBVars

def Lean.Elab.Tactic.Do.BVarUses.add {numBVars : Nat} (a b : BVarUses numBVars) : BVarUses numBVars

instance Lean.Elab.Tactic.Do.instAddBVarUses {numBVars : Nat} : Add (BVarUses numBVars)

def Lean.Elab.Tactic.Do.over1Of2 {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) (x : α₁ × β) : α₂ × β

def Lean.Elab.Tactic.Do.addMData (d : MData) (e : Expr) : Expr

partial def Lean.Elab.Tactic.Do.countUsesDecl (fvarId : FVarId) (ty : Expr) (val? : Option Expr) (bodyUses : FVarUses) (subst : Array FVarId := #[]) : MetaM (Expr × Option Expr × FVarUses)

partial def Lean.Elab.Tactic.Do.countUses (e : Expr) (subst : Array FVarId := #[]) : MetaM (Expr × FVarUses)

def Lean.Elab.Tactic.Do.countUsesLCtx (ctx : LocalContext) (targetUses : FVarUses) : MetaM LocalContext

def Lean.Elab.Tactic.Do.doNotDup (u : Uses) (rhs : Expr) (elimTrivial : Bool) : Bool

def Lean.Elab.Tactic.Do.elimLetsCore (e : Expr) (elimTrivial : Bool := true) : MetaM Expr

def Lean.Elab.Tactic.Do.elimLets (mvar : MVarId) (elimTrivial : Bool := true) : MetaM MVarId