# Documentation

Lean.Compiler.LCNF.Testing

Equations
• One or more equations did not get rendered due to their size.
Instances For
Instances For
• decls :
Instances For
• input :
• output :
Instances For
@[inline]
Equations
Equations
Equations
def Lean.Compiler.LCNF.Testing.SimpleAssertionM.run {α : Type} (decls : ) (passUnderTest : Lean.Compiler.LCNF.Pass) (testName : Lean.Name) :
Equations
def Lean.Compiler.LCNF.Testing.InOutAssertionM.run {α : Type} (input : ) (output : ) (passUnderTest : Lean.Compiler.LCNF.Pass) (testName : Lean.Name) :
Equations
Equations
Equations
Equations
Equations
Equations
def Lean.Compiler.LCNF.Testing.assert (property : Bool) (msg : String) :

If property is false throw an exception with msg.

Equations

Install an assertion pass right after a specific occurrence of a pass, default is first.

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

Install an assertion pass right after each occurrence of a pass.

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

Install an assertion pass right after a specific occurrence of a pass, default is first. The assertion operates on a per declaration basis.

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

Install an assertion pass right after the each occurrence of a pass. The assertion operates on a per declaration basis.

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

Replace a specific occurrence, default is first, of a pass with a wrapper one that allows the user to provide an assertion which takes into account both the declarations that were sent to and produced by the pass under test.

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

Replace all occurrences of a pass with a wrapper one that allows the user to provide an assertion which takes into account both the declarations that were sent to and produced by the pass under test.

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

Insert a pass after passUnderTestName, that ensures, that if passUnderTestName is executed twice in a row, no change in the resulting expression will occur, i.e. the pass is at a fix point.

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

Compare the overall sizes of the input and output of passUnderTest with assertion. If assertion inputSize outputSize is false throw an exception with msg.

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

Assert that the overall size of the Decls in the compilation pipeline does not change after passUnderTestName.

Equations

Assert that the overall size of the Decls in the compilation pipeline gets reduced by passUnderTestName.

Equations

Assert that the overall size of the Decls in the compilation pipeline gets reduced or stays unchanged by passUnderTestName.

Equations

Assert that the pass under test produces Decls that do not contain Expr.const constName in their Code.let values anymore.

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