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
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.
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
Hi,
I wonder if is possible to load proof power from polyML directly, perhaps by
PolyML.make with the proof power source code. The fact is that we want to build
a system which proof power will be in the middle of the architecture, i.e
some_libraries <-- proofpower <-- another_component_with_UI
Yuhui,
On 22 Feb 2013, at 14:24, Yuhui Lin wrote:
> Hi,
>
> I wonder if is possible to load proof power from polyML directly, perhaps by
> PolyML.make with the proof power source code.
I have never tried PolyML.make. There is no reason why you shouldn't compile
the ProofPower source code by l
Hi Rob,
Thanks for you reply. You're right, ProofPower doesn't have to be in the
middle, as there is no dependency. Could you give me some hint about how to
build ProofPower + some_libraries ?
best,
Yuhui
On 22 Feb 2013, at 14:41, Rob Arthan wrote:
> Yuhui,
>
> On 22 Feb 2013, at 14:24,
