def Lean.Meta.Sym.DSimp.beta : DSimproc

Equations

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

def Lean.Meta.Sym.DSimp.zetaDelta (s : FVarIdSet) : DSimproc

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Sym.DSimp.zetaDelta s e = pure Lean.Meta.Sym.DSimp.Result.rfl

def Lean.Meta.Sym.DSimp.zetaDeltaAll : DSimproc

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Sym.DSimp.zetaDeltaAll e = pure Lean.Meta.Sym.DSimp.Result.rfl

def Lean.Meta.Sym.DSimp.zeta : DSimproc

Equations

• Lean.Meta.Sym.DSimp.zeta (Lean.Expr.letE declName type v b nondep) = Lean.Meta.Sym.DSimp.zeta.go✝ (Lean.Expr.letE declName type v b nondep) #[]
• Lean.Meta.Sym.DSimp.zeta e = pure Lean.Meta.Sym.DSimp.Result.rfl

def Lean.Meta.Sym.DSimp.dsimpProj : DSimproc

Equations

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

def Lean.Meta.Sym.DSimp.dsimpMatch : DSimproc

Equations

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