meta.yml

---
fullname: Goedel
shortname: goedel
organization: coq-community
community: true
action: true
coqdoc: false

synopsis: >-
  Coq proof of the Gödel-Rosser 1st incompleteness theorem

description: |-
  A proof in Coq of the Gödel-Rosser 1st incompleteness theorem,
  which says that any first order theory extending NN (which is PA
  without induction) that is complete is inconsistent.

publications:
- pub_url: https://arxiv.org/abs/cs/0505034
  pub_title: Essential Incompleteness of Arithmetic Verified by Coq
  pub_doi: 10.1007/11541868_16

authors:
- name: Russell O'Connor
  initial: true

maintainers:
- name: Pierre Castéran
  nickname: Casteran

opam-file-maintainer: palmskog@gmail.com

opam-file-version: dev

license:
  fullname: MIT License
  identifier: MIT

supported_coq_versions:
  text: 8.13 or later
  opam: '{(>= "8.13" & < "8.17~") | (= "dev")}'

tested_coq_opam_versions:
- version: dev
- version: '8.16'
- version: '8.15'
- version: '8.14'
- version: '8.13'

ci_extra_dev: true

dependencies:
- opam:
    name: coq-hydra-battles
    version: '{= "dev"}'
  description: |-
    [Hydra Battles](https://github.com/coq-community/hydra-battles)
- opam:
    name: coq-coqprime
    version: '{= "dev"}'
  description: |-
    [CoqPrime](https://github.com/thery/coqprime)

namespace: Goedel

keywords:
- name: Goedel
- name: Rosser
- name: incompleteness
- name: logic
- name: Hilbert

categories:
- name: Mathematics/Logic/Foundations

documentation: |-
  ## Documentation

  More information about the project can be found at [this website](http://r6.ca/goedel1.html).
---