k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[K-user] What does the [function] attribute accomplish?

From: Charles Jacobsen <charlie.jacobsen AT utah.edu>
To: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
Subject: [K-user] What does the [function] attribute accomplish?
Date: Wed, 3 Jul 2013 17:33:54 +0000
Accept-language: en-US
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

I've used this for simple "helper functions", but I'm not sure what it does. For example,

syntax Int ::= "countSet" Set [function]
rule countSet .Set => 0
rule countSet SetItem(K:K) S:Set => 1 +Int (countSet S)

This works as expected, but what does the [function] attribute indicate? I couldn't find any info in the overview/primer or by grepping the include dir or source.

[K-user] What does the [function] attribute accomplish?, Charles Jacobsen, 07/03/2013
- Re: [K-user] What does the [function] attribute accomplish?, Radu Mereuta, 07/03/2013
  - Re: [K-user] What does the [function] attribute accomplish?, Rosu, Grigore, 07/03/2013
    - Re: [K-user] What does the [function] attribute accomplish?, Charles Jacobsen, 07/03/2013