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)
Instances For
Instances For
Instances For
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Instances For
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
- Lean.Compiler.LCNF.Testing.getTestName = do let __do_lift ← read pure __do_lift.testName
Instances For
Equations
- Lean.Compiler.LCNF.Testing.getPassUnderTest = do let __do_lift ← read pure __do_lift.passUnderTest
Instances For
Equations
- Lean.Compiler.LCNF.Testing.getDecls = do let __do_lift ← read pure __do_lift.decls
Instances For
Equations
- Lean.Compiler.LCNF.Testing.getInputDecls = do let __do_lift ← read pure __do_lift.input
Instances For
Equations
- Lean.Compiler.LCNF.Testing.getOutputDecls = do let __do_lift ← read pure __do_lift.output
Instances For
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)
Instances For
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.
Instances For
Install an assertion pass right after each occurrence of a pass.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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
Instances For
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
Instances For
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
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.