diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-06-11 01:56:11 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-11 01:56:11 +0200 |
commit | a6d137969a2ddf44f2a51b3465dc62584ca1c026 (patch) | |
tree | 570c46a316306e180933fd744c48f15825af22ab /ide/gtk_parsing.ml | |
parent | 51a56b1aacb516af513de64c00dd7e796f661484 (diff) |
[native_compute] Delay computations with toplevel match
This is an easy improvement on examples like:
Fixpoint zero (n : nat) :=
match n with
| O => O
| S p => zero p + zero p
end.
Definition foo := if true then zero 100 else 0.
Eval native_compute in if true then 0 else foo.
I didn't add a test case, because our current testing infrastructure is too
fragile for that.
Diffstat (limited to 'ide/gtk_parsing.ml')
0 files changed, 0 insertions, 0 deletions