[isabelle] Argument types problem
I am about to definie an inductive set to compute the ste of reachable
states as following:
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
Any helps how to sort out this error please.
This archive was generated by a fusion of
Pipermail (Mailman edition) and