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

v1.15.tar.gz
sha512=f5853d13e06264b67cb8b3c3a3570d651fca80609eb18fdec5739c02a777af4f16b9276ad5150855e4769e74bb36364f6d6c44ec98df33812d553d76eb934ab5

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:2022-07-26

Published: 23 Oct 2022

Dependencies (3)

  1. coq-mathcomp-ssreflect >= "1.12.0" & < "1.18~"
  2. coq >= "8.10" & < "8.17~"
  3. dune >= "2.5"

Dev Dependencies

None

Used by (1)

  1. coq-gaia-ordinals = "1.15"

Conflicts (1)

  1. coq-gaia