hol-light
hol-light copied to clipboard
jrh13
The HOL Light theorem prover
This patch adds `make switch` that - Creates a local OPAM switch under the current hol-light directory - Chooses the latest fully supported OCaml version (4.14 for now; would be...
This PR updates Formal_ineqs to the latest version. The only HOL Light file which is changed (besides files which belong to Formal_ineqs) is `bignum_zarith.ml`: I added the `Big_int` module (which...
Please do not merge this PR but keep it open: its purpose is to provide data on working ocaml-camlp5 pairs. It contains some github action scripts to inventory the pairs...
HOL Light is mostly working okay on OCaml 5, but features that require `update_database.ml` are still missing. The placeholder file is here: https://github.com/jrh13/hol-light/blob/master/update_database_5.ml
Hi. Is there any plan to have hol-light working with recent versions of ocaml and camlp5? See https://github.com/jrh13/hol-light/pull/71.
Probably a naive question: can hol-light be installed as an opam pacakge? If not, why?
Hello. Using ocaml.4.02.3 and campl5.6.17 I get the following problem: ``` #use "hol.ml";; # module OrdInt = struct type t = int let compare = (-) end;; Toplevel input: #...
How do I get out of this without necessarily have to open a new OCaml prompt and reload HOL libs? # ARITH_RULE `(a + x + b * y +...
For example: ``` utop # t1;; - : term = `\x. s x` utop # x1, type_of x1;; - : term * hol_type = (`x`, `:A->bool`) utop # let s1...
File "pa_j.ml", line 413, characters 6-24: 413 | | MtFun loc x1 x2 x3 → ^^^^^^^^^^^^^^^^^^ Error: The constructor MtFun expects 3 argument(s), but is applied here to 4 argument(s)...
