Re: [isabelle] Argument types problem



On Wed, 3 Dec 2014, Ghassen HELALI wrote:

I am about to definie an inductive set to compute the ste of reachable
states as following:

inductive_set
 Reachable :: "[('action,'state)ts, 'state set] ⇒ 'state set" where
    init: "s ∈ Init ==> s ∈ (Reachable Ts Init)"
    | nextStep : "==> [| s ∈ (Reachable Ts Init); (mk_trans s a t) ∈
(trans_of Ts) |] ==> t ∈ (Reachable Ts Init)"

But it was not accepted and I got the following error message:
Argument types ('action, 'state) ts, 'state set of Reachable do not agree
with types of declared parameters

The error message is a bit implicit, meaning that the free parameters Ts and Init should be declared like this:

inductive_set
  Reachable :: "[('action,'state)ts, 'state set] ⇒ 'state set"
  for Ts :: "('action,'state)ts" and Init :: "'state set"


Also note that camel case is not used in Isabelle sources, so nextStep should be next_step.

Moreover, there is no need to put extra parentheses around applications such as (Reachable Ts Init): it binds tightly without that.


	Makarius

----------------------------------------------------------------------------
                  http://stop-ttip.org  998,638 people so far
----------------------------------------------------------------------------


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.