diff options
| author | Pierre-Marie Pédrot | 2018-01-30 13:35:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-02-04 20:08:24 +0100 |
| commit | 1da06b3c3dafaff0d71f36ecf2c732fd90429a86 (patch) | |
| tree | 09c003c431b93d701565b675aaf5d0d4838e3d1d /kernel/nativelambda.mli | |
| parent | 76aff3cbe39da657abb1f559b8ba411a49aab317 (diff) | |
Delay computation of lifts in the reduction machine.
This definitely qualifies as a micro-optimization, but it would not be
performed by Flambda. Indeed, it is unsound in general w.r.t. OCaml
semantics, as it involves a fixpoint and changes potential non-termination.
In our case it doesn't matter semantically, but it is indeed observable
on computation intensive developments like UniMath.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions