Chun Tian

"import declaration not implemented for this Lisp"

9

Hi, I'm trying to compile open-axiom by LispWorks. Basically I modified `core.lisp.in` and related Makefiles (c.f. [1] for details) to support LispWorks. But then I met the following error message...

Hi, This PR intends to make the `iterateTheory` a more fundamental theory without theorems about real numbers. The theory file is now moved to `src/pred_set/src/more_theories`, while the previous real-related materials...

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...

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...

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...

Hi, This PR contains the (finally settled) Rank-based fresh name allocations (implemented in `basic_swapTheory`) and the (reworked) Böhm theory up to Proposition 10.3.7 (i) [1, p.248] (Boehm out lemma). I...

Hi, This PR adds the formalisation of infinite-dimensional Borel space (`Borel_inf`) [1, p.178-179], another important part for the general theory of stochastic processes. One of its alternative definitions depends on...

[listSimps] Improved LIST_EQ_SIMP_CONV knowing SNOC

1

Hi, The conversion `listSimps.LIST_EQ_SIMP_CONV` was able to handle list equations with `SNOC` by first unconditionally normalise all `SNOC` by `SNOC_APPEND`. This is equivalent to hanving `SNOC_APPEND` as part of automatic...

Changed title: `rw` doesn't create abbreviations as in `RW_TAC`

1

Hi, From the implementation of `rw` in `bossLib` (and then `BasicProvers`) it looks that, roughly, `rw = RW_TAC (srw_ss())` but in my practice I found `rw` doesn't do LET-elimination as...