K-user mailing list

[Dwight Guth <dwight.guth AT runtimeverification.com>]

A function rule is similar to a rule tagged "anywhere" in that it applies to any term and not simply at the cell level; it is also different in that it declares its klabel to be a function. What this means is that that klabel is not a constructor for its sort, but instead is required to completely resolve itself into a constructor after one or more applied function rules. As such, only the rules declaring the immediate implementation of the function are allowed to match on that label, and it is an error for any function label to not completely evaluate to a normal (ie non-function) term after applying function rules.

Function rules are also allowed in the latest master to declare an "owise" attribute similar to Maude's, in which a rule is applied if and only if none of the other rules declared for that function match and apply.

On Dec 28, 2014 3:54 PM, "Omar Duhaiby" <3omarz AT gmail.com> wrote:

What does the 'function' label really do to syntax declarations?

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user