k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] when vs require

From: Dwight Guth <dwight.guth AT runtimeverification.com>
To: Markus Knecht <markus.knecht85 AT gmail.com>
Cc: "k-user AT lists.cs.illinois.edu" <k-user AT lists.cs.illinois.edu>
Subject: Re: [[K-user] ] when vs require
Date: Tue, 2 Jan 2018 08:57:11 -0600
Authentication-results: illinois.edu; spf=none smtp.mailfrom=dwight.guth AT runtimeverification.com

They are synonyms of one another.

On Fri, Dec 29, 2017 at 7:37 AM, Markus Knecht <markus.knecht85 AT gmail.com> wrote:

One thing I did not understand in k is the difference between when and require (and the concrete semantics of both). Currently I only use when. But I had the case that when the part behind when is a function that can not be reduced, then it was considered true. Is that intended? and would it behave differently with require?

Re: [[K-user] ] when vs require, Dwight Guth, 01/02/2018