diff options
| author | Enrico Tassi | 2013-12-20 12:23:30 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-04 17:07:15 +0100 |
| commit | a5ebab4f0cd762904055a69b20e6217d08f46637 (patch) | |
| tree | 1aac871466202fb00a7fefd36b16b78ecf76d7a9 /kernel/nativelambda.mli | |
| parent | 0582c9363fa981798811ff11ef0e8c76c38255f7 (diff) | |
Future: allow custom action when a delegated future is forced
The default action is to raise NotReady, but one may want to
make the action "blocking" but successful. Using this device
all delayed proofs can be "delegated". If there are slaves, they
will eventually pick up the task. If there are no slaves, then
the future can behave like a regular, non delegated, lazy computation.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions