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

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

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

Equations

• Lean.Elab.Tactic.Do.instBEqUses = { beq := Lean.Elab.Tactic.Do.beqUses✝ }

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

Equations

• Lean.Elab.Tactic.Do.instOrdUses = { compare := Lean.Elab.Tactic.Do.ordUses✝ }

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

Equations

• Lean.Elab.Tactic.Do.instInhabitedUses = { default := Lean.Elab.Tactic.Do.Uses.zero }

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

Equations

• Lean.Elab.Tactic.Do.Uses.zero.add x✝ = x✝
• x✝.add Lean.Elab.Tactic.Do.Uses.zero = x✝
• x✝¹.add x✝ = Lean.Elab.Tactic.Do.Uses.many

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

Equations

• Lean.Elab.Tactic.Do.Uses.zero.toNat = 0
• Lean.Elab.Tactic.Do.Uses.one.toNat = 1
• Lean.Elab.Tactic.Do.Uses.many.toNat = 2

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

Equations

• Lean.Elab.Tactic.Do.Uses.fromNat 0 = Lean.Elab.Tactic.Do.Uses.zero
• Lean.Elab.Tactic.Do.Uses.fromNat 1 = Lean.Elab.Tactic.Do.Uses.one
• Lean.Elab.Tactic.Do.Uses.fromNat x✝ = Lean.Elab.Tactic.Do.Uses.many

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

Equations

• Lean.Elab.Tactic.Do.instAddUses = { add := Lean.Elab.Tactic.Do.Uses.add }

@[reducible, inline]

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

Equations

• Lean.Elab.Tactic.Do.FVarUses = Std.HashMap Lean.FVarId Lean.Elab.Tactic.Do.Uses

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Tactic.Do.instAddFVarUses = { add := Lean.Elab.Tactic.Do.FVarUses.add }

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) _auto✝ → BVarUses numBVars

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Tactic.Do.BVarUses.none.pop = (Lean.Elab.Tactic.Do.Uses.zero, Lean.Elab.Tactic.Do.BVarUses.none)
• (Lean.Elab.Tactic.Do.BVarUses.some uses).pop = (uses.back, Lean.Elab.Tactic.Do.BVarUses.some uses.pop)

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

Equations

• Lean.Elab.Tactic.Do.BVarUses.none.add b = b
• a.add Lean.Elab.Tactic.Do.BVarUses.none = a
• (Lean.Elab.Tactic.Do.BVarUses.some a_2).add (Lean.Elab.Tactic.Do.BVarUses.some b_2) = Lean.Elab.Tactic.Do.BVarUses.some (Vector.zipWith (fun (a b : Lean.Elab.Tactic.Do.Uses) => a + b) a_2 b_2)

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

Equations

• Lean.Elab.Tactic.Do.instAddBVarUses = { add := Lean.Elab.Tactic.Do.BVarUses.add }

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

Equations

• Lean.Elab.Tactic.Do.over1Of2 f x = (f x.fst, x.snd)

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

Equations

• Lean.Elab.Tactic.Do.addMData d (Lean.Expr.mdata d' e_2) = Lean.Expr.mdata (Lean.KVMap.mergeBy (fun (x : Lean.Name) (new x : Lean.DataValue) => new) d d') e_2
• Lean.Elab.Tactic.Do.addMData d e = Lean.Expr.mdata d e

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Tactic.Do.doNotDup u rhs elimTrivial = (u == Lean.Elab.Tactic.Do.Uses.many && !(elimTrivial && Lean.Elab.Tactic.Do.okToDup✝ rhs))

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.