uds-psl/coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
CoqMPL-2.0
Issues
- 0
Inversion lemma for formulas
#222 opened by Janis-Bai - 16
- 2
- 10
Integration of First-Order Logic
#177 opened by dominik-kirst - 15
Superfluous Minsky Machine Models
#160 opened by mrhaandi - 3
Universe Inconsistencies
#166 opened by mrhaandi - 3
Build fails with 'The term ""hd: empty list"" has type "string" while it is expected to have type "bytestring.string".'
#162 opened by haansn08 - 2
- 3
Definition of undecidability
#119 opened by yforster - 5
- 4
Lemmas of stdlib interest
#118 opened by mrhaandi - 0
Overview graph
#117 opened by yforster - 10
CI launched even if not PR
#112 opened by DmxLarchey - 1
Avoiding Let ... Qed
#102 opened by mrhaandi - 7
- 6
CI cache does not update
#98 opened by mrhaandi - 6
Uncompiled files
#49 opened by fakusb - 0
Compilation Awfully slow over NFS
#66 opened by DmxLarchey - 18
library 1.0.0+8.12 opam release
#81 opened by mrhaandi - 4
coqdoc / website
#92 opened by yforster - 8
Repository structure
#25 opened by yforster - 5
Check commands
#44 opened by yforster - 8
Confusing branches
#73 opened by mrhaandi - 2
"No such goal" in utils_list.v
#62 opened by lbordowitz - 2
- 3
Outdated CeCILL_LICENSE
#38 opened - 1
Reduce the dependencies on metacoq
#14 opened by fakusb