Mark, Yuhui,

On Feb 22, 2013, at 12:47 PM, "Mark" <> wrote:

> That's because ProofPower overwrites PolyML's ML structure List with its
> own, for holding theory about HOL lists.  I'm not sure if anything can be
> done about this without alterning the ProofPower build process (and, say,
> creating a copy of PolyML's List with a name not used by ProofPower).

This is something we (i.e., me, Phil and, I would imagine, a certain Mark now 
of Proof Technologies!) did think about. See below:

> Mark.
> on 22/2/13 12:33 PM, Yuhui Lin <> wrote:
>> Hi,
>> I'm trying to build a programme on the top of proof power with the pp
>> interface. I need a full polyML library from the pp interface, but I can't
>> use some functions which are defined in polyML, e.g List.exists. Any
>> suggestion ?
>> Thanks in advance.

ProofPower was written long before the Standard Basis Library existed. 
Unfortunately, some of the structure names used in ProofPower overwrite 
structures in the Standard Basis Library. In this case, List in ProofPower is 
the structure containing ML bindings relating to the theory of lists.

Many of the Standard Basis Library functions are available in ProofPower's own 
library of ML utilities. See Chapters 2 and 3 of the HOL or Z Reference Manuals 
(usr029 or usr030). There is an equivalent for List.exists called "any" 
(actually ListUtilities.any, but the structure ListUtilities has been opened 
for you).

ProofPower also provides a structure called SML97BasisLibrary that contains all 
the Standard Basis Library structures. So you can get at List.exists as 
SML97BasisLibrary.List.exists as an alternative to ListUtilities.any and you 
can also get at things like List.tabulate that don't have any analogue in the 
ProofPower utilities.

For future reference, you may need to be aware that most of the ProofPower ML 
code that deals with strings is based on the SML'90 treatment of strings 
whereby characters are handled as strings of length 1 rather than as  a 
separate type. Moving to the SML-97 way of handling strings throughout is a 
change I am considering.



>> best,
>> Yuhui
>> --
>> The University of Edinburgh is a charitable body, registered in
>> Scotland, with registration number SC005336.
>> _______________________________________________
>> Proofpower mailing list
> _______________________________________________
> Proofpower mailing list

Proofpower mailing list

Reply via email to