Simplifying Application Arguments

Unlike Sym.Simp.App, dsimp does not need to respect the congruence-info split (fixedPrefix, interlaced, congrTheorem). That split exists in simp to make proof construction efficient — but here there is no proof to build.

dsimp can rewrite every argument, subject only to the rules:

• Skip proof arguments. It is often a waste of time because of proof irrelevance. In some cases, users may want to reduce proofs to eliminate dependencies. Users can accomplish this by rewriting their own simproc.
• Skip instance arguments. Instances are not usually meaningful to simplify structurally. Moreover, we would be producing non-standard instances.

Both classes are read from ProofInstInfo (per-declName, cached in SymM). When the head is not a .const (e.g. an .fvar-headed application), we have no signature info and rewrite every argument.

def Lean.Meta.Sym.DSimp.dsimpAppArgs (e : Expr) : DSimpM Result

Walks the application spine and dsimps each argument unless ProofInstInfo marks it as a proof or instance. The function head itself is not recursively simplified — atomic heads (.const, .fvar) are no-ops anyway, and complex heads can be handled by user-supplied pre/post simprocs.

Equations

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