[ProofPower] any recommended ml editor

2013-02-19 Thread Yuhui Lin
Hi, We plan to start a project based on proofpower. So we want to have a look at the source code, in particular those ml files. I wonder that if there is a recommended editor which can access/organise the source code for a developer. Currently I'm switching between JEditor and vi in xterm,

[ProofPower] ml library functions from pp command line

2013-02-22 Thread Yuhui Lin
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

[ProofPower] load proof power with PolyML

2013-02-22 Thread Yuhui Lin
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.

Re: [ProofPower] load proof power with PolyML

2013-02-22 Thread Yuhui Lin
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 loading it in from

[ProofPower] use library function with special symbol

2013-08-12 Thread YuHui Lin
Hi, I'm currently developing a system on the top of proof power. I get an error when reading a ml file with the keyword use in xpp. The error is caused by the use of a library function containing a special symbol, i.e. dest_simple_%lambda%. I am sure all the codes in the ML file is OK, as

[ProofPower] use and use_file

2013-09-19 Thread YuHui Lin
Hi, I notice that some function names need to be changed when using the key word 'use_file' to include ML files, e.g. EQUAL becomes E%Q%UAL. I wonder why ? Is there anything else I need to keep in mind when using use_fie ? Many thanks. best, Yuhui -- The University of Edinburgh is a

[ProofPower] AVoCS 2015: Second Call for Papers

2015-03-27 Thread YuHui Lin
, Imperial College London, UK Peter Ölveczky, University of Oslo, Norway ORGANISERS Gudmund Grov, Heriot-Watt University, UK Andrew Ireland, Heriot-Watt University, UK Yuhui Lin, Heriot-Watt University, UK (Local arrangements and publicity chair) STEERING COMMITTEE Michael Goldsmith

[ProofPower] AVoCS 2015: Extended Paper Deadline

2015-06-08 Thread YuHui Lin
, UK Andrew Ireland, Heriot-Watt University, UK Yuhui Lin, Heriot-Watt University, UK (local arrangements and publicity chair) STEERING COMMITTEE Michael Goldsmith, University of Oxford, UK Stephan Merz, INRIA Nancy LORIA, France Markus Roggenbach, Swansea University, UK - We

[ProofPower] apply conditional rewriting

2015-06-04 Thread YuHui Lin
Hi, How can I apply a conditional rewrite rule in proof power. For example, applying the following thm: forall x,y, z | x y dot x - y + z = x + z -y where x y is the condition, to generate the following two subgoals: 1) x y 2) goal [x - y + z / x + z -y] Also, I wonder is there any

[ProofPower] error msg when instantiating quantifier in asm

2015-05-28 Thread YuHui Lin
Dear all, I get the following error when I tried to instantiated a forall quantifier in an assumption which I inserted using asm_tac. Exception Fail * Trying to instantiate type variable 'a, which occurs in assumption list [z_∀_elim.6006] * raised The following dummy example can replay this