diff options
Diffstat (limited to 'lib/world.mli')
| -rw-r--r-- | lib/world.mli | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/lib/world.mli b/lib/world.mli index 51ee078..14f82d3 100644 --- a/lib/world.mli +++ b/lib/world.mli @@ -29,11 +29,13 @@ type rule = { rule_name : string; head : Pattern.t Label.Map.t; body : expr; - witness : Label.t option; - (** For a recursive rule, the label whose argument strictly - decreases. The VM requires it ground before unfolding, - which is what turns the admission proof into runtime - termination. [None] on non-recursive rules. *) + witness : Label.t list; + (** For a recursive rule, the lexicographic measure of its + call-graph component: at some position the recursive + argument strictly decreases, all earlier positions staying + equal. The VM requires every position ground before + unfolding, which is what turns the admission proof into + runtime termination. Empty on non-recursive rules. *) } (** The primitive host-checked domains. *) |