maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

[Maude-help] New variables in rule righthand side

From: Diego Marcia <gpimple AT gmail.com>
To: maude-help AT cs.uiuc.edu
Subject: [Maude-help] New variables in rule righthand side
Date: Mon, 10 Nov 2014 20:27:42 +0100
List-archive: <http://lists.cs.uiuc.edu/pipermail/maude-help/>
List-id: <maude-help.cs.uiuc.edu>

Hi,
From maude-manual I read that Conditional Rules are subject to "no restriction on which new variables may appear in the righthand side or the condition".
I'm currently trying to pursue a kind of Invariants Model Checking using meta-level operations such as metaSearch and up/downTerm, but when I try to describe the term I'm searching for using new variables I get the error:
variable MyV:MySort is used before it is bound in rule: <MyRule>

I don't get that. Can someone please explain it to me?

Thanks a lot

Diego Marcia

[Maude-help] New variables in rule righthand side, Diego Marcia, 11/10/2014
- Re: [Maude-help] New variables in rule righthand side, Steven Eker, 11/10/2014