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

Defining help functions for strategies

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.