def Lean.Compiler.LCNF.Simp.simpProj? (e : Lean.Compiler.LCNF.LetValue) : OptionT Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.LetValue

Try to simplify projections .proj _ i s where s is constructor.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Simp.simpProj? e = failure

def Lean.Compiler.LCNF.Simp.simpAppApp? (e : Lean.Compiler.LCNF.LetValue) : OptionT Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.LetValue

Application over application.

let g := f a
g b

is simplified to f a b.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Simp.simpAppApp? e = failure

def Lean.Compiler.LCNF.Simp.simpCtorDiscr? (e : Lean.Compiler.LCNF.LetValue) : OptionT Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.LetValue

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Simp.simpCtorDiscr? e = failure

def Lean.Compiler.LCNF.Simp.applyImplementedBy? (e : Lean.Compiler.LCNF.LetValue) : OptionT Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.LetValue

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Simp.applyImplementedBy? e = do let __do_lift ← read guard (__do_lift.config.implementedBy = true) failure

def Lean.Compiler.LCNF.Simp.simpValue? (e : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.Simp.SimpM (Option Lean.Compiler.LCNF.LetValue)

Try to apply simple simplifications.

Equations

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