Skip to Content.
Sympa Menu

k-user - [K-user] Binding a variable inside "when"

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[K-user] Binding a variable inside "when"


Chronological Thread 
  • From: Charles Jacobsen <charlie.jacobsen AT utah.edu>
  • To: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
  • Subject: [K-user] Binding a variable inside "when"
  • Date: Mon, 24 Jun 2013 17:35:04 +0000
  • Accept-language: en-US
  • List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
  • List-id: <k-user.cs.uiuc.edu>

Hello again,

This module kompiles:

module TEST

  syntax Expr ::= Int "+" Int

  rule I1:Int + I2:Int => S
       when fresh(S:Int)

endmodule

but this one does not:

module TEST

  syntax Expr ::= Int "+" Int

  rule I1:Int + I2:Int => S
       when S:Int ==Int 5

endmodule

Is it not possible to bind a variable in the "when", in general? fresh is just an exception? Perhaps S:Int ==Int 5 is improper.

Thanks, Charlie



Archive powered by MHonArc 2.6.16.

Top of Page