package coq-geocoq-algebraic

  1. Overview
  2. No Docs
A formalization of foundations of geometry in Coq

Install

Dune Dependency

geocoq.github.io Edit opam file Versions (1)

Authors

  1. P
    Pierre Boutry <contact@pierre.boutry.fr>
  2. C
    Cyril Cohen <cyril.cohen@inria.fr>
  3. S
    Stéphane Kastenbaum <stephane.kastenbaum@gmail.com>

Maintainers

  1. P
    Pierre Boutry <contact@pierre.boutry.fr>

Sources

v2.5.0.tar.gz
md5=75609aa3fe8a0fc00cd99c96547775df

Description

This subpackage contains a model of Tarski's axioms and some counter-models.

Tags

category:Mathematics/Geometry/General keyword:geometry keyword:Euclidean geometry keyword:hyperbolic geometry keyword:foundations keyword:Tarski keyword:parallel postulates keyword:model keyword:counter-model keyword:Cartesian space date:2024-03-24

Published: 25 Mar 2024

Dependencies (2)

  1. coq-mathcomp-field >= "1.11.0" & < "2.0~"
  2. coq-geocoq-main = version

Dev Dependencies

None

Used by (2)

  1. coq-geocoq >= "2.5.0"
  2. coq-geocoq-pof >= "2.5.0"

Conflicts (1)

  1. coq-geocoq-pof != version