-
Notifications
You must be signed in to change notification settings - Fork 0
/
meta.yml
83 lines (67 loc) · 1.72 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
---
fullname: Almost Full
shortname: almost-full
organization: coq-community
community: true
action: true
nix: true
coqdoc: false
dune: false
doi: 10.1007/978-3-642-32347-8_17
synopsis: >-
Almost-full relations in Coq for proving termination
description: |-
Coq development of almost-full relations, including the Ramsey
Theorem, useful for proving termination.
publications:
- pub_url: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.225.3021&rep=rep1&type=pdf
pub_title: Stop When You Are Almost-Full
pub_doi: 10.1007/978-3-642-32347-8_17
authors:
- name: Dimitrios Vytiniotis
initial: true
- name: Thierry Coquand
initial: true
- name: David Wahlstedt
initial: true
maintainers:
- name: Karl Palmskog
nickname: palmskog
opam-file-maintainer: palmskog@gmail.com
opam-file-version: dev
license:
fullname: MIT License
identifier: MIT
supported_coq_versions:
text: 8.11 or later
opam: '{>= "8.11"}'
tested_coq_nix_versions:
- coq_version: 'master'
tested_coq_opam_versions:
- version: dev
- version: '8.19'
- version: '8.18'
- version: '8.17'
- version: '8.16'
- version: '8.15'
- version: '8.14'
- version: '8.13'
- version: '8.12'
- version: '8.11'
namespace: AlmostFull
keywords:
- name: Ramsey theorem
- name: termination
- name: almost-full relations
- name: well-founded relations
categories:
- name: Computer Science/Data Types and Data Structures
documentation: |-
## Documentation
Included files:
- `AlmostFull.v`: Basic setup, connections to well-founded relations
- `AFConstructions.v`: Almost-full relation constructions and type-based combinators
- `AlmostFullInduction.v`: Various induction principles
- `AFExamples.v`: Examples
- `Terminator.v`: Deriving the Terminator proof rule
---