[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*Subject*: Question on strategies*From*: Kurt Lichtner <kurt@csg.uwaterloo.ca>*Date*: Thu, 08 Jun 2000 12:01:26 -0400*Delivery-Date*: Thu Jun 8 08:59:27 2000*Sender*: kurt@csl.sri.com

I have what will hopefully be a simple question on defining strategies. I've browsed the archive and chased down some links, but they were not helpful. Given chapter 5 of the PVS Prover Guide, it is straightforward to select all sequent formulae that match some high level connective such as (equality? expr). My question is how do I get more specific. For example, how do I select all equality formulae that use a particular name, such as "c!1", somewhere in the expression representing one of their arguments. For example, I'd like to be able to select formulae like: c!1 = (a,b) or z = c!1`1 Any pointers or advice greatly appreciated, Kurt

- Prev by Date:
**Identical antecedent and consequent** - Next by Date:
**simple problem** - Prev by thread:
**Re: simple problem** - Next by thread:
**proofs involving epsilon** - Index(es):