Documentation

Lean.Compiler.LCNF.Simp.SimpValue

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

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.Expr) :
OptionT Lean.Compiler.LCNF.Simp.SimpM Lean.Expr

Application over application.

let _x.i := f a
_x.i 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.Expr) :
OptionT Lean.Compiler.LCNF.Simp.SimpM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.Simp.applyImplementedBy? (e : Lean.Expr) :
OptionT Lean.Compiler.LCNF.Simp.SimpM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.Simp.simpValue? (e : Lean.Expr) :
Lean.Compiler.LCNF.Simp.SimpM (Option Lean.Expr)

Try to apply simple simplifications.

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