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.16.tar.gz
sha512=694dfe2a60896a4b044854c612cc54462e92864349f35d7b87b6ab40878260d0400d406b8657ac8fed39ae7b27b58ba3b9c9c12082adbf0313d270abfd494dc5

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:2023-11-18

Published: 18 Nov 2023

Dependencies (1)

  1. coq >= "8.16" & < "8.21"

Dev Dependencies

None

Used by

None

Conflicts

None