partial def findENatAtoms (e : Q(ℕ∞)) : Mathlib.Tactic.AtomM Unit

@[inline]

def Lean.Expr.or? (p : Expr) : Option (Expr × Expr)

Equations

• p.or? = p.app2? `Or

partial def parse (e : Lean.Expr) : Mathlib.Tactic.AtomM Unit

def atoms (g : Lean.MVarId) : Mathlib.Tactic.AtomM (Array Lean.Expr)

Equations

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

def Array.zipLeft {α : Type} (l : Array α) (ns : Array Lean.Name) : Array (α × Option Lean.Name)

Equations

• l.zipLeft ns = (l.toList.zipLeft ns.toList).toArray

def generalizeAtoms (ns : Array Lean.Name) (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

Equations

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

def tacticGeneralize_enatsWith___ : Lean.ParserDescr

Equations

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

def tacticGeneralize_enats : Lean.ParserDescr

Equations

• tacticGeneralize_enats = Lean.ParserDescr.node `tacticGeneralize_enats 1024 (Lean.ParserDescr.nonReservedSymbol "generalize_enats" false)

def tacticEnat_to_nat! : Lean.ParserDescr

Equations

• tacticEnat_to_nat! = Lean.ParserDescr.node `tacticEnat_to_nat! 1024 (Lean.ParserDescr.nonReservedSymbol "enat_to_nat!" false)

def tacticEomega : Lean.ParserDescr

Equations

• tacticEomega = Lean.ParserDescr.node `tacticEomega 1024 (Lean.ParserDescr.nonReservedSymbol "eomega" false)

def tacticEnat_to_nat!With___ : Lean.ParserDescr

Equations

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

Replacing enat_to_nat.

Tinkering

Oddities