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).
Mark. on 22/2/13 12:33 PM, Yuhui Lin <[email protected]> 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. > > best, > Yuhui > -- > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. > > _______________________________________________ > Proofpower mailing list > [email protected] > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > > _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
