HOL

HOL copied to clipboard

Fix intLib to avoid noisy output

1

Following commit f6c3ef2, loading intLib produces a lot of output that should be suppressed and/or avoided (see below). Ideally there should not be calls to Meson when loading the library....

acjf3

Hi, This PR ports the ring decision procedure (`RING_TAC` and `RING_RULE`) from HOL-Light ([`ringtheory.ml`](https://github.com/jrh13/hol-light/blob/master/Library/ringtheory.ml)). The ring decision procedure, currently located at `examples/algebra/ring/ringLib.sml`, can be used to decide equations about ring...

binghe

C++ compilation failure of `src/HolSat/sat_solvers/zc2hs` on macOS

1

I think this issue is new on macOS 14 (Sonoma) with latest Xcode (I'm using version 15.3). Apple's `c++` (`clang++`) cannot compile `src/HolSat/sat_solvers/zc2hs/zc2hs.cpp`: ``` src/HolSat/sat_solvers/zc2hs$ make ln -fs ../minisat/Proof.o ln...

binghe

A broken generated HTML theory in non-Unicode mode

2

Hi, It seems that for each core theory there are two HTML pages generated in the help page. One is that you directly click the theory names from the HOL...

binghe

`Q.PAT_X_ASSUM` (_aka_ `qpat_x_assum`) returns bad error messages because its implementation can't distinguish between an expected failure (the pattern not matching an unrelated assumption) and an unexpected failure (the continuation failing)....

mn200

Suggestion from @myreen on Discord: > Could there be general-purpose quote filter support for making this nicer? Specifics can be discussed, but something along these lines: ``` val cakeml_code =...

mn200

Can be useful to match on a sub-term of an assumption.

mn200

It should be possible to specialise variables without knowing where in a quantification block they are, and if free, the effect can be as of `INST`.

mn200

Something like ``` simp[IgnAsm ‘pat’, th1] ``` should apply the simplifier, while ignoring the assumption(s) matching `pat`. Also ``` simp[NoAsms,...] ``` should ignore all assumptions.

mn200

intLib.{ARITH,COOPER}_PROVE can't prove certain goals

5

I'm running into an issue where both `intLib.ARITH_PROVE` and `intLib.COOPER_PROVE` are failing to prove certain goals, even though it seems like they should be able to handle them. Here are...

someplaceguy