package coq-gaia-schutte

  1. Overview
  2. No Docs
Implementation of ordinals in Coq following Schütte and Ackermann

Install

Dune Dependency

github.com Edit opam file Versions (5)

Authors

  1. J
    José Grimm
  2. A
    Alban Quadrat

Maintainers

  1. P
    palmskog@gmail.com

Sources

v2.2.tar.gz
sha512=e025071a0e1a3aa5b9bd484913ecda39e4448a34f8d22c8eb3f7e03ce4e65012c2169bc1ce8c4410727fa8a6a4a0debfe6c3772a77b162e0adbbd1acf5a36c2d

Description

Types for ordinal numbers in Coq using the Mathematical Components library, following the approaches of Schütte and Ackermann.

Tags

category:Mathematics/Arithmetic and Number Theory/Number theory keyword:ordinal arithmetic keyword:ordinal numbers logpath:gaia.schutte date:2024-07-24

Published: 11 Aug 2024

Dependencies (3)

  1. coq-mathcomp-ssreflect >= "2.0"
  2. coq >= "8.16"
  3. dune >= "3.5"

Dev Dependencies

None

Used by (1)

  1. coq-gaia-ordinals >= "2.2"

Conflicts (1)

  1. coq-gaia