package coq-high-school-geometry

  1. Overview
  2. No Docs
Geometry in Coq for French high school

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. F
    Frédérique Guilhot
  2. T
    Tuan-Minh Pham

Maintainers

  1. P
    palmskog@gmail.com

Sources

v8.13.tar.gz
sha512=47dba843c3541c628725224b6f9d353b5e5d224cd16ae52d6980a6aec9d698855477934609364dfaaa91271818f530d7af6d344c2ee7c38f8c0e0a3e226a655e

Description

This Coq library is dedicated to high-shool geometry teaching. The axiomatisation for affine Euclidean space is in a non analytic setting. Includes a proof of Ptolemy's theorem.

Tags

category:Mathematics/Geometry/General keyword:geometry keyword:teaching keyword:high school keyword:Ptolemy's theorem logpath:HighSchoolGeometry date:2021-08-06

Published: 06 Aug 2021

Dependencies (1)

  1. coq >= "8.12" & < "8.16~"

Dev Dependencies

None

Used by

None

Conflicts

None