Definitional reduction simprocs

Sym.simp versions of the reduction steps in Lean.Meta.Sym.Reduce. The proof of each step is Eq.refl of the result, which the kernel accepts because the terms are definitionally equal.

def Lean.Meta.Sym.Simp.beta : Simproc

Beta-reduces applications with a lambda head.

Equations

• Lean.Meta.Sym.Simp.beta e = do let __do_lift ← liftM (Lean.Meta.Sym.reduceBeta? e) liftM (Lean.Meta.Sym.Simp.ofReduce?✝ __do_lift)

def Lean.Meta.Sym.Simp.zeta : Simproc

Zeta-reduces let/have telescopes.

Equations

• Lean.Meta.Sym.Simp.zeta e = do let __do_lift ← liftM (Lean.Meta.Sym.reduceZeta? e) liftM (Lean.Meta.Sym.Simp.ofReduce?✝ __do_lift)

def Lean.Meta.Sym.Simp.zetaDelta (s : FVarIdSet) : Simproc

Unfolds the let-bound free variables in s at head position.

Equations

• Lean.Meta.Sym.Simp.zetaDelta s e = do let __do_lift ← liftM (Lean.Meta.Sym.reduceZetaDelta? e (Std.TreeSet.contains s)) liftM (Lean.Meta.Sym.Simp.ofReduce?✝ __do_lift)

def Lean.Meta.Sym.Simp.zetaDeltaAll : Simproc

Unfolds every let-bound free variable at head position.

Equations

• Lean.Meta.Sym.Simp.zetaDeltaAll e = do let __do_lift ← liftM (Lean.Meta.Sym.reduceZetaDelta? e) liftM (Lean.Meta.Sym.Simp.ofReduce?✝ __do_lift)

def Lean.Meta.Sym.Simp.reduceProj : Simproc

Reduces projection functions applied to constructors.

Equations

• Lean.Meta.Sym.Simp.reduceProj e = do let __do_lift ← liftM (Lean.Meta.Sym.reduceProjApp? e) liftM (Lean.Meta.Sym.Simp.ofReduce?✝ __do_lift)

def Lean.Meta.Sym.Simp.reduceMatcher : Simproc

Iota-reduces match and recursor applications whose discriminants are constructors.

Equations

• Lean.Meta.Sym.Simp.reduceMatcher e = do let __do_lift ← liftM (Lean.Meta.Sym.reduceMatcherApp? e) liftM (Lean.Meta.Sym.Simp.ofReduce?✝ __do_lift)