Skip to Main content Skip to Navigation

GeoCoq

Abstract : A formalization of geometry in Coq. This library contains a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high-school.
Complete list of metadata

Browse

Present sur SoftwareHeritage
swh:1:dir:97ce53176b7d5e89d069bc60f49c3fa186831307;origin=https://hal.archives-ouvertes.fr/hal-01912024;visit=swh:1:snp:1cbf6e8cee9dde43b03c16566f00122653381227;anchor=swh:1:rev:640e8d6a4813be6b44bee473dfb674f40daac1f0;path=/

https://hal.inria.fr/hal-01912024
Contributor : Julien Narboux <>
Submitted on : Monday, November 5, 2018 - 3:30:38 PM
Last modification on : Wednesday, June 26, 2019 - 4:29:43 PM

Share

Metrics

Record views

250

Files downloads

5