partial def Lean.Compiler.LCNF.Code.containsConst (constName : Lake.Name) (code : Lean.Compiler.LCNF.Code) : Bool

partial def Lean.Compiler.LCNF.Code.containsConst.goExpr (constName : Lake.Name) (e : Lean.Expr) : Bool

def Lean.Compiler.LCNF.Code.containsConst.goLetValue (constName : Lake.Name) (l : Lean.Compiler.LCNF.LetValue) : Bool

structure Lean.Compiler.LCNF.Testing.TestInstallerContext : Type

• passUnderTestName : Lake.Name
• testName : Lake.Name

structure Lean.Compiler.LCNF.Testing.TestContext : Type

• passUnderTest : Lean.Compiler.LCNF.Pass
• testName : Lake.Name

structure Lean.Compiler.LCNF.Testing.SimpleAssertionContext : Type

• decls : Array Lean.Compiler.LCNF.Decl

structure Lean.Compiler.LCNF.Testing.InOutAssertionContext : Type

• input : Array Lean.Compiler.LCNF.Decl
• output : Array Lean.Compiler.LCNF.Decl

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Testing.TestInstallerM (α : Type) : Type

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Testing.TestInstaller : Type

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Testing.TestM (α : Type) : Type

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Testing.SimpleAssertionM (α : Type) : Type

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Testing.InOutAssertionM (α : Type) : Type

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Testing.SimpleTest : Type

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Testing.InOutTest : Type

def Lean.Compiler.LCNF.Testing.TestInstaller.install (x : Lean.Compiler.LCNF.Testing.TestInstaller) (passUnderTestName : Lake.Name) (testName : Lake.Name) : Lean.Compiler.LCNF.PassInstaller

def Lean.Compiler.LCNF.Testing.TestM.run {α : Type} (x : Lean.Compiler.LCNF.Testing.TestM α) (passUnderTest : Lean.Compiler.LCNF.Pass) (testName : Lake.Name) : Lean.Compiler.LCNF.CompilerM α

def Lean.Compiler.LCNF.Testing.SimpleAssertionM.run {α : Type} (x : Lean.Compiler.LCNF.Testing.SimpleAssertionM α) (decls : Array Lean.Compiler.LCNF.Decl) (passUnderTest : Lean.Compiler.LCNF.Pass) (testName : Lake.Name) : Lean.Compiler.LCNF.CompilerM α

def Lean.Compiler.LCNF.Testing.InOutAssertionM.run {α : Type} (x : Lean.Compiler.LCNF.Testing.InOutAssertionM α) (input : Array Lean.Compiler.LCNF.Decl) (output : Array Lean.Compiler.LCNF.Decl) (passUnderTest : Lean.Compiler.LCNF.Pass) (testName : Lake.Name) : Lean.Compiler.LCNF.CompilerM α

def Lean.Compiler.LCNF.Testing.getTestName : Lean.Compiler.LCNF.Testing.TestM Lake.Name

def Lean.Compiler.LCNF.Testing.getPassUnderTest : Lean.Compiler.LCNF.Testing.TestM Lean.Compiler.LCNF.Pass

def Lean.Compiler.LCNF.Testing.getDecls : Lean.Compiler.LCNF.Testing.SimpleAssertionM (Array Lean.Compiler.LCNF.Decl)

def Lean.Compiler.LCNF.Testing.getInputDecls : Lean.Compiler.LCNF.Testing.InOutAssertionM (Array Lean.Compiler.LCNF.Decl)

def Lean.Compiler.LCNF.Testing.getOutputDecls : Lean.Compiler.LCNF.Testing.InOutAssertionM (Array Lean.Compiler.LCNF.Decl)

def Lean.Compiler.LCNF.Testing.assert (property : Bool) (msg : String) : Lean.Compiler.LCNF.Testing.TestM Unit

If property is false throw an exception with msg.

def Lean.Compiler.LCNF.Testing.assertAfter (test : Lean.Compiler.LCNF.Testing.SimpleTest) (occurrence : optParam Nat 0) : Lean.Compiler.LCNF.Testing.TestInstaller

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

def Lean.Compiler.LCNF.Testing.assertAfterEachOccurrence (test : Lean.Compiler.LCNF.Testing.SimpleTest) : Lean.Compiler.LCNF.Testing.TestInstaller

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

def Lean.Compiler.LCNF.Testing.assertForEachDeclAfter (assertion : Lean.Compiler.LCNF.Pass → Lean.Compiler.LCNF.Decl → Bool) (msg : String) (occurrence : optParam Nat 0) : Lean.Compiler.LCNF.Testing.TestInstaller

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

def Lean.Compiler.LCNF.Testing.assertForEachDeclAfterEachOccurrence (assertion : Lean.Compiler.LCNF.Pass → Lean.Compiler.LCNF.Decl → Bool) (msg : String) : Lean.Compiler.LCNF.Testing.TestInstaller

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

def Lean.Compiler.LCNF.Testing.assertAround (test : Lean.Compiler.LCNF.Testing.InOutTest) (occurrence : optParam Nat 0) : Lean.Compiler.LCNF.Testing.TestInstaller

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.

def Lean.Compiler.LCNF.Testing.assertAroundEachOccurrence (test : Lean.Compiler.LCNF.Testing.InOutTest) : Lean.Compiler.LCNF.Testing.TestInstaller

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.

def Lean.Compiler.LCNF.Testing.assertIsAtFixPoint : Lean.Compiler.LCNF.Testing.TestInstaller

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.

def Lean.Compiler.LCNF.Testing.assertSize (assertion : Nat → Nat → Bool) (msg : String) : Lean.Compiler.LCNF.Testing.TestInstaller

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

def Lean.Compiler.LCNF.Testing.assertPreservesSize (msg : String) : Lean.Compiler.LCNF.Testing.TestInstaller

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

def Lean.Compiler.LCNF.Testing.assertReducesSize (msg : String) : Lean.Compiler.LCNF.Testing.TestInstaller

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

def Lean.Compiler.LCNF.Testing.assertReducesOrPreservesSize (msg : String) : Lean.Compiler.LCNF.Testing.TestInstaller

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

def Lean.Compiler.LCNF.Testing.assertDoesNotContainConstAfter (constName : Lake.Name) (msg : String) : Lean.Compiler.LCNF.Testing.TestInstaller

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

def Lean.Compiler.LCNF.Testing.assertNoFun : Lean.Compiler.LCNF.Testing.TestInstaller