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

Re: Rewrite rules don't rewrite this equality.

John Hoffman writes:
 > > I think most of the information from strategies.lisp can be accessed
 > > via the x-prover-command window.  
 > > 
 > I miss the source.  It was very useful for us when we developed some
 > strategies in house.  We learned how to access the proof state by
 > examining the lisp definitions of the strategies.

If you highlight a command in the x-prover-command window and click
the right mouse button, you will get the lisp definition for that
strategy (i.e. the body from the defstep).  You won't be able to get
the source for the support functions, but that hasn't been available
in strategies.lisp either.

Also, I'm not sure if the definitions in strategies.lisp are current.
The last time I checked (about a year ago), I noticed that the lisp
source from x-prover-command was different from that in the (then
available) strategies.lisp file.

-- Paul S. Miner                | email: p.s.miner@larc.nasa.gov
-- 1 South Wright St. / MS 130  |   fax: (757) 864-4234
-- NASA Langley Research Center | phone: (757) 864-6201
-- Hampton, Virginia 23681-0001 |