[ProofPower] any recommended ml editor

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, neit

[ProofPower] ml library functions from pp command line

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

[ProofPower] load proof power with PolyML

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

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 comp

[ProofPower] use library function with special symbol

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 th

[ProofPower] use and use_file

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 charita

[ProofPower] AVoCS 2015: First Call for Papers

g, Altran, UK John Wickerson, 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

[ProofPower] AVoCS 2015: Second Call for Papers

Wallenburg, Altran, UK John Wickerson, 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

[ProofPower] building error and solution regarding the x11 path for Mac

Hi, I’ve got two errors when I install pp, on the latest version of Mac OS 10.10.2. The causes of these two errors are the path of X11 which seems to be different. I am thinking my experience might be helpful, so I share the errors and the fixes here. The error messages I got are 'X11

Re: [ProofPower] building error and solution regarding the x11 path for Mac

Hi Rob, > It looks to me like you have the Apple X11 files in /opt/X11, but not the > MacPorts X11 stuff in /opt/local. Yes. I install the Apple X11 but not the MacPorts X11. > So where do you have OpenMotif installed? Where does configure say it found > Motif? I installed OpenMotif through fin

[ProofPower] AVoCS 2015: Final Call for Papers

tran, UK John Wickerson, 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

[ProofPower] error msg when instantiating quantifier in asm

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

[ProofPower] apply conditional rewriting

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] AVoCS 2015: Extended Paper Deadline

NISERS 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, University of Oxford, UK Stephan Merz, INRIA Nancy & LORIA, France Markus Roggenba