Simon Cruanes

I think more kinds of steps might be good, if you handle the TSTP output and llproof checker properly (which I assume is the whole point anyway). In that case...

I mean, it's an inference, but the llprover must handle it differently (namely, by not using `opaque` for the assumptions, otherwise it's not obvious why it's a tautology). It could...

I have absolutely no idea.

Awesome. So far I'm impressed by how clean the bindings are :grin:

That looks simply amazing. I'll give it a try when I'm off work. Thank you!! edit: tried the demo, it works directly. Very nice.

They're not very usable, sorry. The imgui API is big, my code generation is complicated because I tried to generate ctypes with the multiple layers of code generation (to avoid...

`of_seq` is easy, it's `to_seq` that'd be hard.

Is that the same primitive that mtime exposes?

maybe a dune variant to provide the clock implementation could help? One could provide a mtime-based variant, for exotic architectures where it's better supported (which might be no better than...

I think providing a hashtable of `key, elements with this key` would be great, except that it's less convenient to express in OCaml as you cannot return a polymorphic hashtable....