This looks great, Vincent.
Are you interested in working on a version for HOL4?
On Thu, Jul 11, 2013 at 11:08 AM, Vincent Aravantinos <
vincent.aravanti...@gmail.com> wrote:
> Hi list,
>
> I developed a new tactic that takes a theorem of the form P ==> l = r and
> replaces l by r in a goal addin
HOL Light has a decent body of theory about cardinality inequalities and
arithmetic for sets-as-predicates.
For example, see
https://code.google.com/p/hol-light/source/browse/trunk/sets.ml#2774 and
https://code.google.com/p/hol-light/source/browse/trunk/Library/card.ml#171onwards.
As far as I know
Thanks - that looks very useful!
On Fri, Aug 9, 2013 at 8:57 AM, Michael Norrish <
michael.norr...@nicta.com.au> wrote:
> There's a chunk of stuff in examples/set-theory/hol_sets/cardinalTheory,
> including, for example, the fact that k x k = k.
>
> Michael
>
> On
>From what I remember, camlp5 and ocaml versioning is a nightmare... (though
it may be that HOL Light is a particularly strenuous application for it).
One might find Alex Krauss's approach useful:
http://sourceforge.net/mailarchive/message.php?msg_id=29220282, if going at
the pa_j.ml file doesn't h
Hi Andrea, and welcome! We'd be very happy to answer your questions :)
The installation problem you're having is likely due to building Poly/ML
without the --enable-shared flag (passed to the configure script).
Did you build Poly/ML from source, or was it packaged by your distribution?
Version 5.5
Hi Vincent,
I strongly advise against this solution. Moscow ML is much slower than
Poly/ML, and some features of HOL4 don't work with it (e.g. heaps).
However, with a language defined by a standard we would always hope to be
implementation-agnostic :)
Cheers,
Ramana
On Wed, Oct 16, 2013 at 6:4
Another option would be to use an older version of Poly/ML, e.g. 5.5.
There was some discussion about this issue on the Poly/ML mailing list,
around this thread:
http://lists.inf.ed.ac.uk/pipermail/polyml/2013-September/001344.html
On Wed, Oct 16, 2013 at 6:49 PM, Ramana Kumar wrote:
>
ask questions there.
If we can't get ownership of that channel, ##hol is available.
> Thanks again,
>
> Andrea
>
>
> On 16/10/13 18:54, Ramana Kumar wrote:
>
> Another option would be to use an older version of Poly/ML, e.g. 5.5.
> There was some discussion about thi
Hi everyone,
I have registered the #hol channel on the freenode network, and invite
anyone interested to join it to provide and receive support on using HOL
(and HOL Light etc.). It would be a real-time counterpart to this mailing
list.
(There is some help linked from freenode.net if you haven't
The variable `t` in your goal cannot be generalised, for the same reason
that you can't generalise variables that appear free in the assumptions of
a theorem.
I think the goalstack you showed is unproveable. But it looks like you
probably did an induction without using a general enough induction
h
to
>> obtain R (t,u) ==> ?v. R (t,v) /\ R (u,v), then
>> 2) with MP from the new 0: R (t,u) ==> ?v. R (t,v) /\ R (u,v) and the
>> assumption 1: R (t',u), obtain ?v. R (t',v) /\ R (u,v) which is just the
>> goal.
>>
>> The problem is that I want to gener
There's no easy way to do this, that I know of, but there are several
difficult ways.
The simplest is: try removing the theorem from the list you give to
METIS_TAC (or RW_TAC) and see if the proof still goes through or not.
This is a trial and error approach, so is a bit tedious, but is at least
s
; There is a flag implemented so that the simplifier
> tracks which rules are successfully applied. See
>
>simpLib.{track,track_rewrites,used_rewrites}
>
> Konrad.
>
>
>
> On Fri, Oct 25, 2013 at 3:47 PM, Ramana Kumar wrote:
>
>> There's no easy way to
Hmm... this could be a throwback to a time when the hypotheses were
represented by a list... if so the documentation should be updated. I'm not
entirely sure though.
On Thu, Dec 5, 2013 at 5:19 PM, Rob Arthan wrote:
> Ramana assures me that HOL4 manages the assumptions of a theorem as a set
> m
I'm not sure I understand what the problem is. Perhaps you could show
us something that you want to prove but cannot prove?
The term you showed looks fine to me for a double integral.
It doesn't matter if "x" in "(\x. f x * y) : real -> real" is
unbounded, because "integral (a,b)" puts the bounds
This is a great idea, I'm glad you are planning to write something.
Two resources that come to mind are the existing HOL4 Tutorial that
comes with the distribution (I presume you already saw this?), and
also Magnus Myreen's guide
http://www.cl.cam.ac.uk/~mom22/HOL-interaction.pdf.
On Wed, Jan 29,
;0 <= a /\ &0 <= b /\ integrable (&0,b) f
> ==> (integral(&0,a)(\y. integral(&0,y)(\x.f x * y ) ) = integral(&0,a)(\y.
> integral(&0,y)(\x.f x)* y ))`;
> the problem is this proof needs condition "&0 <= y", but I can't proof it
> from
Hi all,
I am trying to use EmitML to generate ML for a function of type char list
-> string that does pattern matching on its first argument. The generated
ML currently looks like
fun foo "" = ...
| foo (c::cs) = ...
and the generated signature says foo : string -> string.
I would like (ind
, Capital Normal University (CNU)
Beijing, China
On Sat, Feb 1, 2014 at 10:59 AM, yefengleng wrote:
> Thank you for your reply, I have not figure this problem. Could you
> explain it in some detail?
>
>
> 2014-01-31 Ramana Kumar :
>
> Did you figure
Is there a way to find the precedence/fixity information about a token in
the term grammar that is better than using Parse.term_grammar() and sifting
through the voluminous output? Sometimes I don't have enough scroll buffer
to catch what I need from that!
--
ements on the HOL Light version in the
> coming weeks hopefully, and then I plan indeed to "translate" it to HOL4.
>
> V.
>
>
> 2013/7/30 Ramana Kumar
>
>> This looks great, Vincent.
>> Are you interested in working on a version for HOL4?
>>
>>
ded in the manual are a good starting point to grasp a
> lil bit better the intended behaviour. Dunno if that helps though.
> Unfortunately, on a daily basis, I use only the HOL Light version of it
> and could not test on real-life use cases the HOL4 version :-(
>
> Cheers,
> V.
&
You could use some tactical that pulls out an assumption (POP_ASSUM,
FIND_ASSUM, FIRST_ASSUM, USE_THEN, REMOVE_THEN, etc.) and give it a trivial
thm_tactic like (K ALL_TAC) to essentially ignore (and hence discard) the
assumption and do nothing else.
On Thu, Feb 13, 2014 at 4:03 AM, Adnan Rashid
You are right, Bill. Thank you. FIRST_X_ASSUM rather than FIRST_ASSUM,
definitely. In HOL4 POP_ASSUM deletes the assumption, but I'm not sure if
it's the same in HOL Light - perhaps not.
On Fri, Feb 14, 2014 at 1:12 PM, Bill Richter wrote:
> Ramana, I think it's better to say that the one time
CALL FOR ABSTRACTS
2014 International Workshop on HOL4
The HOL Theorem Proving System
(HOL'14)
hosted by ITP at FLoC
July 13, 2014, Vienna, Austria
http://vsl2014.at/pages/HOL-i
The constant = is not defined in HOL Light, but simply declared (as Mark
said). In fact, equality is even more basic than that: it's a built in
term. You can see, for example, the "safe_mk_eq" function in fusion.ml, and
also the "the_term_constants" reference (which starts with "=" built in).
I fe
I believe it takes several hours. I haven't done it myself though.
On Sat, Apr 5, 2014 at 3:23 AM, Jiaqi Tan wrote:
> Hi,
>
> I have downloaded the latest version of HOL from github, and my current
> build of examples/machine-code is taking quite a long time, and the build
> has been stuck in e
Perhaps SELECT_ELIM_TAC?
On Thu, Apr 10, 2014 at 6:23 AM, Adnan Rashid
<14dphditaras...@seecs.edu.pk>wrote:
> Dear all,
>
> I am working in HOL-Light. I am having an equation and on the right side
> of equation, I am having Hilbert choice operator (@). How to remove this
> Hilbert choice operato
I find this very counterintuitive:
> load"listLib";
val it = (): unit
> computeLib.CBV_CONV (listLib.list_compset()) ``EXISTS P []``;
<>
val it = |- EXISTS P [] ⇔ EXISTS P []: thm
whereas:
> EVAL ``EXISTS P []``;
<>
val it = |- EXISTS P [] ⇔ F: thm
I also don't understand why it is happening.
B
Could it be that listSimps.sml is picking up EXISTS_DEF from boolTheory
rather than from listTheory?
On Mon, Apr 14, 2014 at 3:16 PM, Ramana Kumar wrote:
> I find this very counterintuitive:
>
> > load"listLib";
> val it = (): unit
> > computeLib.CBV_CONV (lis
Using listTheory.EXISTS_DEF in listSimps.sml does not seem to help. I would
appreciate (dis)confirmation.
On Mon, Apr 14, 2014 at 3:26 PM, Ramana Kumar wrote:
> Could it be that listSimps.sml is picking up EXISTS_DEF from boolTheory
> rather than from listTheory?
>
>
> On Mon, Ap
Thanks for the analysis Albert.
This issue has been fixed by Anthony Fox in
e84a11e8adcc0f0dd0fc8936a7df8bf61f4f9fc5.
On Mon, Apr 14, 2014 at 8:05 PM, Albert Y. C. Lai wrote:
> On 14-04-14 10:26 AM, Ramana Kumar wrote:
> > Could it be that listSimps.sml is picking up EXISTS
I'm about to write a conversion to reduce terms of the form Num(&n) where n
is a ground non-negative integer. But I would expect such a thing to
already exist somewhere - does anyone know where?
I notice that EVAL does not reduce Num(&1) - is there something I can load
that will make it do so?
---
oops, the title of this thread should be NUM_OF_INT conversion, and then no
conversion is needed: it's just a rewrite... still, it should be a rewrite
that's in the int compset surely?
On Tue, Apr 15, 2014 at 7:30 AM, Ramana Kumar wrote:
> I'm about to write a conversion to r
exist yet.
On Tue, Apr 15, 2014 at 7:42 AM, Ramana Kumar wrote:
> oops, the title of this thread should be NUM_OF_INT conversion, and then
> no conversion is needed: it's just a rewrite... still, it should be a
> rewrite that's in the int compset surely?
>
>
> On Tue,
, Ramana Kumar wrote:
> Turns out I was confused again, this time by commonUnif$Num shadowing
> integer$Num.
>
> The thing I actually want is something to reduce ``Num n`` to ``n`` where
> n is a non-negative numeral (it has different types in the two quotations).
> That's proba
CALL FOR ABSTRACTS
2014 International Workshop on HOL4
The HOL Theorem Proving System
(HOL'14)
hosted by ITP at FLoC
July 13, 2014, Vienna, Austria
http://vsl2014.at/pages/HOL-i
I suspect lcsymtacs.rfs[] (aka REV_FULL_SIMP_TAC (srw_ss()) []) will do it
in your particular example.
Alternatively, you could use REPEAT BasicProvers.VAR_EQ_TAC THEN
FULL_SIMP_TAC std_ss [].
These will all change your goal state in more ways than one.
On Tue, May 13, 2014 at 9:01 AM, masoume
One more way of doing it, which actually uses modus ponens more directly:
let open lcsymtacs in
first_x_assum(fn th => first_assum (strip_assume_tac o MATCH_MP th))
end
On Tue, May 13, 2014 at 9:25 AM, Ramana Kumar wrote:
> I suspect lcsymtacs.rfs[] (aka REV_FULL_SIMP_TAC (srw_ss()) []
gs of computeLib. It’s looking as if
> my initial understanding of the behaviour of set_skip is wrong. Will have
> to do some more experiments. - Anthony
> >
> > On 17 May 2013, at 09:34, Ramana Kumar
> wrote:
> >
> >> Please go ahead and make this change then
The name of the constant you defined is "sum_cube", not "sum_cube_def" as
in your goal.
On Sat, May 24, 2014 at 10:58 AM, Valerie Martin wrote:
> I am trying to prove the following sum:
>
> 1^3 + 2^3 + 3^3 .. n^3 = (n^2 (n+1)^2) / 4
>
> I have made the following function for the left side
>
> v
CALL FOR PARTICIPATION
HOL'14 at FLoC'14
July 13, 2014
Vienna Summer of Logic
A Workshop on the
HOL Theorem Proving System
Info: http://vsl2014.at/meetings/HOL-index.html
We welcome anyone with
Hi David,
I think you could prove your goal with METIS_TAC[EQ_TC_SETS]. (Or even
METIS_TAC[TC_RULES].)
Alternatively, you could do STRIP_TAC THEN MATCH_MP EQ_TC_SETS and
simplification would probably take it from there.
Ramana
On Thu, May 29, 2014 at 5:39 PM, David Sanan wrote:
> Hi all,
> I
Hi all,
I suspect there's a nice way to get the munger to print datatypes in the
syntax accepted by the new Datatype command (i.e. without all the "of"s,
and perhaps with better line-breaking), but I can't figure it out right
now. Does anyone know?
Ideally I'm looking for instructions for how to
Is there a nice way to add user printers to pretty-print lists of different
types differently?
We've tried using add_user_printer on the pattern ``ls:foo list``, but this
seems to apply the user printer on other kinds of lists as well.
Looking at the implementation of user printers it seems like
first_x_assum(qspec_then`1`mp_tac)
On Thu, Jul 10, 2014 at 3:02 PM, David Sanan wrote:
> Hi all,
>
>
> I am trying to prove this goal and n=1 in assumption 2 is a counterexample
> leading to ¬(¬TCn R n x x ∨ ∃n'. TCn R n' x x ∧ n' < n), where TCn is the
> NRC relation without reflexivity and ∀
HOL's pretty-printer usually prints the empty list as "[]", which I believe
is produced by two separate tokens (one for each bracket) via a "listform"
parsing/printing rule.
In LaTeX math mode (generated using HOL's math mode munger) "[]" does not
look nice: it needs a bit of space inside. What wo
By default the munger doesn't do anything special to strings; the usual
pretty-printing behaviour is to print the elements of the string without
any separators between double-quotes. In math mode, the contents of the
string thus are treated as LaTeX variables and appear in italics with too
much spa
empty
lists?
I tried prefer_form_with_tok but it didn't work.
On Thu, Jul 24, 2014 at 3:47 PM, Michael Norrish <
michael.norr...@nicta.com.au> wrote:
> The latter is how I've done this in the past.
>
> Michael
>
> > On 24 Jul 2014, at 22:16, "Ramana Kumar"
mmar when TeX-pretty-printing was due to happen. This would allow
> maximum
> flexibility because the normal-use grammars wouldn’t get contaminated at
> all,
> and weird pretty-printing stuff could be kept in its own silo. You can
> emulate
> this a little at the moment by creating
cked up by the concrete syntax phase (only "NIL" is).
>
I see.
>
> Normal lists will print as per the list-form rule.
>
> Michael
>
> On 25/07/14 16:10, Ramana Kumar wrote:
> > I am already using a special "pretty-printing" theory when creating my
>
hat various literal forms were handled specially.
>
> Michael
>
> On 25/07/14 01:04, Ramana Kumar wrote:
> > By default the munger doesn't do anything special to strings; the usual
> > pretty-printing behaviour is to print the elements of the string without
> any
>
Is there some way to turn off the "Saved theorem" etc. messages during a
build of HOL? I notice there's a "--quiet" option for Holmake (although not
for bin/build), but it seems not to suppress very much.
--
Infragistics Pr
I don't personally know of anything about matrix multiplication in HOL, but
hopefully someone else might...
Even if there's nothing in HOL, perhaps is some theory in HOL Light or
Isabelle/HOL that could be ported?
Same for LFSR and polynomials over finite fields.
On Mon, Aug 11, 2014 at 9:41 AM,
Hi Jiaqi Tan,
You will need to prove the first two conjuncts at some point. The second
one is already an assumption, so that's easy, but the first one looks like
it might be false. If you can prove them, then the remaining conjunct
(SPEC) should indeed be true by the SPEC_FRAME theorem. One way yo
Hi all,
Yong Kiam showed me something very useful today, so I'd like to share it
with you all. If you're using HOL with Poly/ML, then there are functions
PolyML.SaveState.saveState and PolyML.SaveState.loadState, both of type
string -> unit, which save the state of the REPL in a file (the string i
Hi Nela,
I've written about this before, you might find the following message (and
the links inside it) useful:
http://www.mail-archive.com/hol-info@lists.sourceforge.net/msg02358.html
For HOL Light developers, I would like to issue a request: would it be so
difficult to remove the dependence on
Glad to hear Nix might be working out for you. It is a very nice package
management idea.
I actually meant to refer you to the HOL Light Workbench (see
http://www.mail-archive.com/hol-info@lists.sourceforge.net/msg01558.html)
which you might have missed since it was several clicks away from the li
Hi all,
I'm having trouble figuring out how to add theorems that include string
literals into my LaTeX document, when the strings might contain a
backslash. The munger produces something like:
\HOLStringLit{\\/}
which, when inside a math environment, confuses LaTeX a lot.
Does anyone have an id
You could use Joe Hurd's fork of HOL Light that adds support for recording
and exporting proofs in OpenTheory article format.
See http://gilith.com/research/opentheory/ and
http://src.gilith.com/hol-light.html.
On Sat, Oct 11, 2014 at 3:34 AM, Mario Carneiro wrote:
> Hello,
>
> I'm interested in
When I make a munger with monadsyntax and use it to typeset some monadic
functions, the "do" and "od" delimiters of a list of binds are emitted
as-is. I would like them to be annotated as HOLKeywords.
I know I could probably use the override map for that, but it seems like
there ought to be a more
Hi all,
There has been an interesting discussion on the OpenTheory mailing list
recently regarding how to simplify the two theorems produced by a type
definition in HOL Light and remove their free variables. The latest message
in the thread, which shows the suggestions by Mario Carneiro can be fo
Hi all,
I would like to add a pretty-printing rule to completely omit a constructor
and only print its argument. (I understand this means the resulting output
won't parse back to the same input without type inference help.) Is it
possible to do this in any way short of making a userprinter?
To be
hu, Oct 23, 2014 at 10:54 PM, Michael Norrish <
michael.norr...@nicta.com.au> wrote:
>
>
> > On 24 Oct 2014, at 04:59, Ramana Kumar
> wrote:
>
> > (Userprinters are very difficult to use with the munger, so I would
> like to avoid them if possible.)
>
> Why
On Mon, Jan 26, 2015 at 12:54 PM, Jiaqi Tan wrote:
> Hi,
>
> I have some questions regarding the internals of HOL4, and whether there
> are any internal resources (memory/storage) used when certain functions are
> used.
>
There are at least two kinds of resources that are relevant when
consideri
Is it possible to merge duplicate (or alpha-convertible) subgoals during a
proof, to reduce the total number of subgoals? Maybe using list tactics?
--
Dive into the World of Parallel Programming. The Go Parallel Website,
sp
I often run into this kind of error:
Holmake: Analysing fooTheory.sml
Warning - Unable to increase stack - interrupting thread
Fail exception: Got an Interrupt exception, with message in
make_up_to_date
especially when fooTheory.sml is large (10s of MBs).
As I understand it, Holmake is merely t
r
> worse now.
>
> Michael
>
> On 03/02/15 22:45, Ramana Kumar wrote:
> > I often run into this kind of error:
> >
> > Holmake: Analysing fooTheory.sml
> > Warning - Unable to increase stack - interrupting thread
> > Fail exception: Got an Int
ols.)
>
> You should run unquote on the input file first to mimic what Holdep does
> (and
> the quotations would confuse the Holdep lexer if left to be seen by it).
>
> Michael
>
> On 04/02/15 09:29, Ramana Kumar wrote:
> > Yes, I saw those changes and hoped things might ha
ool replSideTheory.sml.unquote 0.92s user
0.02s system 98% cpu 0.961 total
On Wed, Feb 4, 2015 at 9:56 AM, Ramana Kumar wrote:
> OK, most of the problem files are in bootstrap/translation/repl of the
> CakeML repository.
> Here's an example using holdeptool and crashing:
>
> rk436@
I'm having a lot of trouble getting Holmake to work when I have
dependencies included (via INCLUDES in my Holmakefile). Has something
substantial changed in how I'm supposed to write a Holmakefile? It seems
like Holmake is using the INCLUDES from my current directory even when it
makes recursive ca
Related to this: are relative paths allowed in the INCLUDES? and in that
case, shouldn't they be relative to the directory containing the
Holmakefile?
On Wed, Feb 18, 2015 at 11:21 AM, Ramana Kumar
wrote:
> I'm having a lot of trouble getting Holmake to work when I have
> depen
rsion), it is clearly broken in some
> cases.
>
> Michael
>
>
> > On 19 Feb 2015, at 4:03 am, Ramana Kumar
> wrote:
> >
> > Related to this: are relative paths allowed in the INCLUDES? and in that
> case, shouldn't they be relative to the directory conta
227f470.
>
> Best,
> Michael
>
> On 19/02/15 17:46, Ramana Kumar wrote:
> > Here is how to create a small test case that breaks:
> >
> > dir:
> > my1Script.sml
> >
> > dir/bar
> > Holmakefile - INCLUDES = foo
> > m
I'm having a lot of trouble trying to remove a type abbreviation when using
the HOL->TeX munger. I make the munger with a main theory that calls
Parse.disable_tyabbrev_printing "reln". And if I load this theory in an
interactive HOL session and type ``:'a -> 'a -> bool`` it prints back as I
expect.
x27;ve added test-cases to src/TeX/theory_tests (see commit 29db124)
> indicating
> that scenarios like yours seem to be behaving as expected.
>
> Michael
>
> On 06/03/15 05:33, Ramana Kumar wrote:
> > I'm having a lot of trouble trying to remove a type abbreviati
Is this something different from what Hol_reln will give you?
On Tue, Mar 10, 2015 at 6:33 PM, Muhammad Qasim
wrote:
> Hello Everyone,
>
> I saw an inductive_set definition in Isabelle. Is there a way to do
> such definitions in HOL4?
>
> Thank you.
>
> Regards
>
> Qasim
>
>
>
>
>
> and it gives me unification failure. I guess it is different.
>
> Regards
>
> Qasim
>
> Quoting Ramana Kumar :
>
> > Is this something different from what Hol_reln will give you?
> >
> > On Tue, Mar 10, 2015 at 6:33 PM, Muhammad Qasim <
> m_q...@enc
One method is editor integration, which makes the process of viewing the
proof less painful than manual copy-paste.
In HOL4 there is integration for both Vim (
https://github.com/HOL-Theorem-Prover/HOL/tree/master/tools/vim) and Emacs,
which might be a suitable starting point. (These essentially j
There is an example of a nominal datatype in
HOL4/examples/unification/triangular/nominal.
On Wed, Mar 18, 2015 at 4:10 PM, Petros Papapanagiotou
wrote:
> Hello everyone,
>
> Having reached the ceiling of what I can achieve by "hacking" variable
> bindings and substitutions for embedded language
I remember once hearing about some checks that can be done on theorems when
they are saved, such as ensuring that quantified variables actually occur.
Does anyone know where the code for these checks can be found (presuming
they exist) and how to turn them on?
--
CALL FOR ABSTRACTS
2015 International Workshop on HOL4
The HOL Theorem Proving System
(HOL'15)
hosted by CADE-25
August 2-3, 2015, Berlin, Germany
https://www.cl.cam.ac.uk/~rk4
SECOND CALL FOR ABSTRACTS
2015 International Workshop on HOL4
The HOL Theorem Proving System
(HOL'15)
hosted by CADE-25
August 2-3, 2015, Berlin, Germany
https://www.cl.cam.ac.uk
In both cases it sounds like the problem is that rewriting is rewriting too
much - you only want to rewrite a particular occurrence of a term.
You might try using ONCE_REWRITE_RULE or Once.
If that doesn't work, you can be much more specific about where you apply
rewriting by using the rewriting co
Another option is to abbreviate the parts of the term that you don't want
to be rewritten. See Q.PAT_ABBREV_TAC for example.
On 21 May 2015 at 13:12, Ramana Kumar wrote:
> In both cases it sounds like the problem is that rewriting is rewriting
> too much - you only want to rewrite a
Hi all,
A reminder: the deadline for abstracts for the upcoming HOL4 Workshop is
less than one week away. All details can be found at the website:
https://www.cl.cam.ac.uk/~rk436/hol15/
We look forward to receiving your abstracts, and to seeing you in Berlin
for the workshop!
---
Dear all,
I warmly invite you to participate in the upcoming HOL workshop, co-located
with CADE. It promises to be an exciting opportunity to learn about,
discuss, and work on the HOL theorem prover and the CakeML verified
programming language, and to shape future developments and integrations
wit
What is the difference between these functions?
Parse.overload_on
Parse.Unicode.uoverload_on
Parse.Unicode.unicode_version
Which ones should be used when? Does more than one need to be used at once?
>From some of my recent playing around, it seems like unicode_version
sometimes but not always req
Having just run into problems with type abbreviations again, I want to
bring issues #148, #168, and #265 to the attention of anyone interested in
solving them.
I especially note that #168 has an open bounty on it, so you stand to make
some money by closing it.
https://github.com/HOL-Theorem-Prove
Hi all,
I think this must be some neat combination of category theory things.
Does anyone know which? Or if it's already defined somewhere?
val map_option_def = Define`
(map_option [] = SOME []) ∧
(map_option (NONE::_) = NONE) ∧
(map_option (SOME x::ls) =
case map_option ls of
| SOME
o possible.
>
> Both types, ie, 'a option set, and 'a set option, are compound monads, and
> your function is a monad morphism, which is also used in a certain
> construction which can be used to prove that the latter is indeed a
> compound monad.
>
> Cheers,
>
&
uld be worth putting monad-related definitions and
> theorems in HOL theory files such as list, option? Then one might consider
> extending this to certain compound monads.
>
> Cheers,
>
> Jeremy
>
> On 26/09/15 09:56, Ramana Kumar wrote:
>
>> Hi Jeremy,
>>
&g
I just wanted to share that thanks to Thibault Gauthier, holyhammer
(integrated powerful ATP provers) is already quite useful in HOL4.
I put this in my .hol_config:
fun hh_tac g =
(holyHammer.hh[](list_mk_imp g); ALL_TAC g);
Then I can run hh_tac when I get stuck at a goal but think it should
Is there any theory about partial orders in HOL4?
I have been party to some work on the partial order of lazy lists under the
prefix relation (in particular proving that it is complete). It would be
nice to instantiate (or create?) some general theory, although going too
far in that direction prob
To my surprise, EVAL went into a loop on the following term:
``WHILE (\x. x = 0) (\x. x) 1``
I thought in the default setup, EVAL would only evaluate the first argument
of a conditional, reducing it to true or false, skipping the other
arguments (the then and else branches) until it was known whic
5ed0
>
> Michael
>
> On 13 Oct 2015, at 14:57, Yong Kiam wrote:
>
> I tried it and got the same problem BUT it only occurred after I opened
> integerTheory.
>
> Additionally, ``WHILE (\x.x=(0:num)) (\x.x) 1`` evals fine.
>
> On Tue, Oct 13, 2015 at 11:11 AM, Ramana Kumar
Dear HOL users and developers,
I will endeavour to organise a workshop for HOL, to be co-located with ITP
2016 (France, end of August).
Before planning the details, I want to ask you: what kind of workshop would
serve you best?
Please send me any requests or comments, and together we can use thi
You forgot to mention the comprehensive Vim mode for HOL4.
(See tools/vim in the HOL4 repository.)
On 4 November 2015 at 16:22, Joe Leslie-Hurd wrote:
> For those of you who use HOL Light in an Emacs shell, I wrote some
> simple Emacs Lisp macros to support interactive proof:
>
> https://github.c
I have this problem again. Can anyone help?
% camlp5 -v
Camlp5 version 6.14 (ocaml 4.02.3)
hol-light % make
\
if test `ocamlc -version | cut -c1-3` = "3.0" ; \
then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1
Use computeLib.EVAL.
On 14 November 2015 at 13:23, shengyu shen wrote:
> Dear all:
>
> I have some experience in ACL2 and COQ, which have a programming mode, in
> which I can try running some function. For example, I define a fact
> function that compute the factorial of a particular integer n.
1 - 100 of 313 matches
Mail list logo
