Documentation

Lean.Compiler.LCNF.Simp.SimpValue

source
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.
source
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.
source
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.
source
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.
source
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.