Equations
- Lean.Compiler.LCNF.Code.containsConst.goLetValue constName (Lean.Compiler.LCNF.LetValue.value value) = false
- Lean.Compiler.LCNF.Code.containsConst.goLetValue constName Lean.Compiler.LCNF.LetValue.erased = false
- Lean.Compiler.LCNF.Code.containsConst.goLetValue constName (Lean.Compiler.LCNF.LetValue.proj typeName idx struct) = false
- Lean.Compiler.LCNF.Code.containsConst.goLetValue constName (Lean.Compiler.LCNF.LetValue.fvar fvarId args) = false
- Lean.Compiler.LCNF.Code.containsConst.goLetValue constName (Lean.Compiler.LCNF.LetValue.const name us args) = (name == constName)
Equations
- Lean.Compiler.LCNF.Testing.getTestName = do let __do_lift ← read pure __do_lift.testName
Equations
- Lean.Compiler.LCNF.Testing.getPassUnderTest = do let __do_lift ← read pure __do_lift.passUnderTest
Equations
- Lean.Compiler.LCNF.Testing.getDecls = do let __do_lift ← read pure __do_lift.decls
Equations
- Lean.Compiler.LCNF.Testing.getInputDecls = do let __do_lift ← read pure __do_lift.input
Equations
- Lean.Compiler.LCNF.Testing.getOutputDecls = do let __do_lift ← read pure __do_lift.output
If property
is false
throw an exception with msg
.
Equations
- Lean.Compiler.LCNF.Testing.assert property msg = if property = true then pure PUnit.unit else Lean.throwError ((Lean.MessageData.ofFormat ∘ Std.format) msg)
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 Decl
s in the compilation pipeline does not change
after passUnderTestName
.
Equations
- Lean.Compiler.LCNF.Testing.assertPreservesSize msg = Lean.Compiler.LCNF.Testing.assertSize (fun (x1 x2 : Nat) => x1 == x2) msg
Assert that the overall size of the Decl
s in the compilation pipeline gets reduced by passUnderTestName
.
Equations
- Lean.Compiler.LCNF.Testing.assertReducesSize msg = Lean.Compiler.LCNF.Testing.assertSize (fun (x1 x2 : Nat) => decide (x1 > x2)) msg
Assert that the overall size of the Decl
s in the compilation pipeline gets reduced or stays unchanged
by passUnderTestName
.
Equations
- Lean.Compiler.LCNF.Testing.assertReducesOrPreservesSize msg = Lean.Compiler.LCNF.Testing.assertSize (fun (x1 x2 : Nat) => decide (x1 ≥ x2)) msg
Assert that the pass under test produces Decl
s 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.