This project implements lemmas and theorems on hyper-operations in Coq.
A CoqDoc generated file can be found here.
This project was inspired by "The Fundamental Theorems of Hyper-Operations" by Renny Barrett, available online here.
Barrett, R. The Fundamental Theorems of Hyper-Operations. Preprints 2019, 2019020176 (doi: 10.20944/preprints201902.0176.v1).
I am not affiliated with Renny Barrett, nor anyone else involved in the creation of this paper.
Most theorems and lemmas presented here come directly from the paper, and are explicitly marked as such in the source code. Their proofs are often based on the proofs in the paper as well; that said, my primary focus was on making them work in Coq rather than translating them exactly, so they may diverge from the paper. All I've done is translate the ideas into Coq.
The original paper is distributed under a Creative Commons CC BY license.