maximedenes/native-coq — Issue #6: Lazy evaluation of values
Author: maximedenes
Created: 2011-12-14 13:26:31+00:00
State: open

Values defined at toplevel should be evaluated in a lazy fashion:

Definition n := fact 100.
Eval native_compute in true.

Should answer instantly "true".