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.12.tar.gz
sha512=9ea14ee20c690e844f8180c270c1e99985bd2d3128f61be1948c1eef9dfc8870f7c45553f1f6b4d7a3f9354900ce110f9eddba9f7a05abae85db160ad8f438b8

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:2020-10-19

Published: 20 Oct 2020

Dependencies (1)

  1. coq >= "8.11" & < "8.13~"

Dev Dependencies

None

Used by

None

Conflicts

None