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

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

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

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

• passUnderTestName : Name
• testName : Name

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

• passUnderTest : Pass
• testName : Name

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

• decls : Array Decl

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

• input : Array Decl
• output : Array Decl

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

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

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

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

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

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

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

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

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

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

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

If property is false throw an exception with msg.

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

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

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

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

def Lean.Compiler.LCNF.Testing.assertForEachDeclAfter (assertion : Pass → Decl → Bool) (msg : String) (occurrence : Nat := 0) : 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 : Pass → Decl → Bool) (msg : String) : 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 : InOutTest) (occurrence : Nat := 0) : 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 : InOutTest) : 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 : 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) : 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) : 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) : 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) : 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 : Name) (msg : String) : 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 : TestInstaller