def Blaster.logReprExpr (msg : String) (e : Lean.Expr) : Optimize.TranslateEnvT Unit

Log the representation of e when verbose is set to 3.

Equations

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

def Blaster.logPPExpr (msg : String) (e : Lean.Expr) : Optimize.TranslateEnvT Unit

Pretty print and log e when verbose is set to 3.

Equations

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

def Blaster.logSmtQuery : Optimize.TranslateEnvT Unit

Dumps to stdout the smt commands submitted to the backend solver when option dumpSmtLib is set to true.

Equations

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

@[inline]

def Blaster.profileTask {α : Type} (msg : String) (p : Optimize.TranslateEnvT α) (verboseLevel : Nat := 1) : Optimize.TranslateEnvT α

Profile Task msg when verbose is greater than verboseLevel by displaying the time taken by msg.

Equations

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