before, just by expanding definitions:
val lemma = Q.prove
(`!n A j. A (j) = system n A (j)`,
RW_TAC arith_ss
[system_def, replace_smaller_def,combinTheory.APPLY_UPDATE_THM]);
Konrad.
On Sun, Apr 14, 2013 at 7:23 AM, J. J. W. bsc.j@gmail.com wrote:
Dear all,
thank you for your
Dear all,
I have a small question regarding loading SML files, I have some
difficulties loading them using hol.bat from the hol installer for Windows.
I have written a file with the following contents:
(* Test loading file *)
set_trace Unicode 0;
val test = Define `identityList a = a`;
Now I
be, then you may have to go back and restate the goal, or even,
eventually,
re-adjust your notion of what is really needed to obtain success.
Konrad.
On Mon, Apr 15, 2013 at 8:52 AM, J. J. W. bsc.j@gmail.com wrote:
Dear Konrad,
thank you for your explanation. So I tried something
,
Konrad.
On Thu, Apr 11, 2013 at 6:10 AM, J. J. W. bsc.j@gmail.com wrote:
Dear all,
I would like to model the following:
public replace_smaller(int[] A, int c, int d){
if (A[d] A[c]){
A[c] = A[q]
}
return A;
}
and I would like to prove
Dear all,
I would like to model the following:
public replace_smaller(int[] A, int c, int d){
if (A[d] A[c]){
A[c] = A[q]
}
return A;
}
and I would like to prove that the resulting array is just like the code.
So I think I should define the following:
val replace_smaller_def = Define
ram...@member.fsf.org
On Tue, Feb 5, 2013 at 8:17 PM, J. J. W. bsc.j@gmail.com wrote:
Dear all,
I am using Mint 13 and already have installed PolyML 5.5 successfully.
I've executed the following commands:
Mint hol # poly 'home/user/Downloads/hol/tools/smart-configure.sml
Dear all,
I am using Mint 13 and already have installed PolyML 5.5 successfully. I've
executed the following commands:
Mint hol # poly 'home/user/Downloads/hol/tools/smart-configure.sml'
...
Finished configuration!
val it = (): unit
That worked perfectly since it completed the configuration,
