@palmskog @Zimmi48

goedel is a great contribution, and is worth maintaining !

Nevertheless, if we want to use it also as a library of primitive recursive functions (for instance in coq-hydra-battles), there is a lot of work to be done.

• add documentation (files of examples, coqdoc comments, text), especially for functions defined by interactive proofs.
• add tactics
• use "modern" coq style (bullets, implicit arguments, type classes, ...)

I created a branch new-stuff for these improvements (which may take a long time)

Given that there are changes planned upstream to the Ackermann library in hydra-battles (coq-community/hydra-battles#31), this could be a good time to make a timestamp/release of goedel that works with hydra-battles 0.4 and Coq 8.13 (and 8.12). After the release, we can restrict this project to 8.13+ like hydra-battles.

@Casteran what do you think? I can do the release if you think it's a good idea.

FWIW, the compilation of Goedel fails with Coq 8.14 with the following error:

 File "./theories/chRem.v", line 257, characters 0-6:
Error: The reference double was not found in the current environment.

@palmskog

I tried to install coq-goedel as indicated on the README, but it seems to be compatible only with CoqV8.10