package coq-hydra-battles

  1. Overview
  2. No Docs
Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq

Install

Dune Dependency

github.com Edit opam file Versions (4)

Authors

  1. P
    Pierre Castéran

Maintainers

  1. P
    palmskog@gmail.com

Sources

v0.4.tar.gz
sha256=bba82794e49e03fd82fcee592b2b037ec20669d10e6c47ed8b4f8a7f851756eb

Description

An exploration of some properties of Kirby and Paris' hydra battles, with the help of the Coq Proof assistant. This development includes the study of several representations of ordinal numbers, and a part of the so-called Ketonen and Solovay machinery (combinatorial properties of epsilon0).

Tags

category:Mathematics/Combinatorics and Graph Theory category:Mathematics/Logic/Foundations keyword:Ketonen-Solovay machinery keyword:ordinal numbers keyword:primitive recursive functions logpath:hydras date:2021-05-19

Published: 08 Jun 2021

Dependencies (1)

  1. dune >= "2.5"

Dev Dependencies (2)

  1. coq-equations (>= "1.2" & < "1.3~") | (= "dev")
  2. coq (>= "8.11" & < "8.14~") | (= "dev")

Used by (2)

  1. coq-gaia-hydras < "0.6"
  2. coq-goedel >= "8.13.0"

Conflicts

None