Recent Releases of trocq
trocq - Trocq 0.2.0
This release of Trocq's prototype works with both Coq/Rocq stdlib and HoTT.
- Rocq Prover
Published by CohenCyril 9 months ago
trocq - Trocq 0.1.8+prop
This is a demo release of Trocq, based on standard Coq/Rocq rather than HoTT. Support for Prop has been added together with temporary axioms for proof irrelevance and prop extensionality. The examples of this version are improved.
- Rocq Prover
Published by CohenCyril about 1 year ago
trocq - Trocq 0.1.7+prop
This is a demo release of Trocq, based on standard Coq/Rocq rather than HoTT. Support for Prop has been added together with temporary axioms for proof irrelevance and prop extensionality.
- Rocq Prover
Published by CohenCyril over 1 year ago
trocq - Trocq 0.1.6
This is a demo version of Trocq.
- Rocq Prover
Published by CohenCyril almost 2 years ago
trocq - Trocq 0.1.5
This is a demo version of Trocq.
- Rocq Prover
Published by CohenCyril about 2 years ago
trocq - Trocq 0.1.4
This is a demo version of Trocq.
- Rocq Prover
Published by CohenCyril about 2 years ago
trocq - Trocq 0.1.3
This is a demo version of Trocq.
- Rocq Prover
Published by CohenCyril about 2 years ago
trocq - Trocq 0.1.1
This is a demo version of Trocq.
- Rocq Prover
Published by CohenCyril about 2 years ago
trocq - Trocq 0.1.0
This is a demo version of Trocq, compatible with Coq 8.17 with Coq-HoTT and using a custom version of Coq-Elpi.
- Rocq Prover
Published by CohenCyril about 2 years ago