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

*To*: pvs-help@csl.sri.com*Subject*: Defining help functions for strategies*From*: Steve Johnson <sjohnson@cs.indiana.edu>*Date*: Thu, 18 Jan 2001 13:51:20 -0500 (EST)

I use PVS in an introductory senior-level course. The students are veteran Scheme users but have not used CL. In a project playing with PVS strategies, several groups expressed a desire to add basic list-processing help functions (e.g. flatten a tree, things like that). Which direction should I take? * Always be more clever with strategies, except maybe for I/O. * Probably, they could do enough of what they need to do with with FUNCTION, MAP, and MAPCAR and quasiquote in the LET bindings (i.e. iteration)? This is not to subvert the prover, just to organized subgoals. * Maybe there's a way to use local DEFUNs of some kind in strategies, but I don't know how to do it in CL/CLOS/PVS.

- Prev by Date:
**Re: infix-problem** - Next by Date:
**Trivial proofs and set lemmas** - Prev by thread:
**Re: Trivial proofs and set lemmas** - Next by thread:
**infix-problem** - Index(es):