opaque auto.redMode : Lean.Option Lean.Meta.TransparencyMode

opaque auto.mono.tyRed.mode : Lean.Option Lean.Meta.TransparencyMode

opaque auto.mono.tyDefEq.mode : Lean.Option Lean.Meta.TransparencyMode

def Auto.unfoldProj (e : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Auto.unfoldProj e = pure e

def Auto.prepReduceExprWithMode (term : Lean.Expr) (mode : Lean.Meta.TransparencyMode) : Lean.MetaM Lean.Expr

Equations

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

def Auto.prepReduceExpr (term : Lean.Expr) : Lean.MetaM Lean.Expr

This function is expensive

Equations

• Auto.prepReduceExpr term = do let __do_lift ← Lean.getOptions let mode : Lean.Meta.TransparencyMode := Lean.Option.get __do_lift auto.redMode Auto.prepReduceExprWithMode term mode

def Auto.prepReduceDefeq (type : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

We assume that all defeq facts have the form ∀ (x₁ : ⋯) ⋯ (xₙ : ⋯), c ... = ... where c is a constant. To avoid whnf from reducing c ⋯ (which can happen when e.g. c is a recursor), we call forallTelescope, then call prepReduceExpr on · All the arguments of c, and · The right-hand side of the equation

Equations

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

def Auto.prepReduceTypeForall (e : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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