Adrien Champion

`-tool` mode ill-formed on some exceptions

3

## Description When printing certain exceptions, TLC introduces a newline `\n` between the exception's description and the `:` preceding the context in which the exception was raised. *Apparently* this is...

I'm getting started on this code base and find it difficult to understand as there is no documentation or tests. After some discussion with [@lefessant](https://github.com/lefessan) I started documenting/doc-testing the code....

feat: migrate List lemmas from mathlib

14

Integrates a few of Mathlib's lemmas over `List`s. Some proofs have been slightly simplified

set-option print-success true has no effect

4

Is there any plan to add print-success? It could be interesting for tools interacting with solvers _via_ system pipes.

Adds accessors to inner `Arc` ref and to the weak count closes #15

`weak_table` optional dependency with adequate `WeakElement` implementation

2

We prefer not adding dependencies if we can avoid it, but at least two users expressed interest in integrating with [`weak_table`] (#15). While there is a reasonable workaround, actual integration...

Add timeout/heartbeat feature

1

Would be great to add either a timeout option, or a "heartbeat" one (limit on the number of instructions executed, does not depend on the machine it's running on). In...

Hoice's error-handling is based on [`error-chain`](https://crates.io/crates/error-chain) and has several issues as far as Hoice is concerned. The main problem is that `error-chain` erases errors, *i.e.* [`rsmt2`](https://crates.io/crates/rsmt2)'s errors become `dyn std::error::Error`...

bump to 4.8.0-rc1

2

I'm starting to use lean-auto, and noticed it does not require `std`'s `stable` branch but `main` instead, which does not build as it's now in 4.8.0-rc1. I have a version...

more `Int` and `Rat` lemmas - most `Int` lemmas are only useful for proofs over `Rat`-s