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

Equations

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

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

Unfolds the let-bound free variables in s at head position. See Sym.reduceZetaDelta?.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.Sym.DSimp.dsimpProj e = do let __do_lift ← liftM (Lean.Meta.Sym.reduceProjApp? e) pure (Lean.Meta.Sym.DSimp.ofReduce?✝ __do_lift)

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

Equations

• Lean.Meta.Sym.DSimp.dsimpMatch e = do let __do_lift ← liftM (Lean.Meta.Sym.reduceMatcherApp? e) pure (Lean.Meta.Sym.DSimp.ofReduce?✝ __do_lift)

def Lean.Meta.Sym.DSimp.unfold (declNames : NameSet) : DSimproc

Unfolds the applications of the definitions in declNames, like Meta.simp does for the definitions provided in simp [f]. A definition with smart unfolding support is unfolded only when its recursion argument reduces. Any other definition is unfolded only when applied to at least as many arguments as its number of leading lambdas.

Equations

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