-
Notifications
You must be signed in to change notification settings - Fork 7
/
meta.yml
119 lines (99 loc) · 3.26 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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
---
fullname: Gaia
shortname: gaia
organization: coq-community
community: true
dune: false
action: true
synopsis: Implementation of books from Bourbaki's Elements of Mathematics in Coq
description: |-
Implementation of books from N. Bourbaki's Elements of Mathematics
in Coq using the Mathematical Components library, including set theory
and number theory.
build: |-
## Building and installation
To build and install manually, do:
``` shell
git clone https://github.com/coq-community/gaia.git
cd gaia
make # or make -j <number-of-cores-on-your-machine>
make install
```
publications:
- pub_url: https://jfr.unibo.it/article/view/1899
pub_title: "Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets"
pub_doi: 10.6092/issn.1972-5787/1899
- pub_url: https://jfr.unibo.it/article/view/4771
pub_title: "Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers"
pub_doi: 10.6092/issn.1972-5787/4771
- pub_url: https://hal.inria.fr/inria-00408143
pub_title: "Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets"
- pub_url: https://hal.inria.fr/inria-00440786
pub_title: "Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers"
- pub_url: https://hal.inria.fr/hal-01412037
pub_title: "Implementation of Bourbaki's Elements of Mathematics in Coq: Part Three Structures"
- pub_url: https://hal.inria.fr/hal-01093589
pub_title: "Fibonacci numbers and the Stern-Brocot tree in Coq"
- pub_url: https://hal.inria.fr/hal-00911710
pub_title: "Implementation of three types of ordinals in Coq"
authors:
- name: José Grimm
- name: Alban Quadrat
- name: Carlos Simpson
maintainers:
- name: Laurent Théry
nickname: thery
opam-file-maintainer: palmskog@gmail.com
opam-file-version: dev
license:
fullname: MIT License
identifier: MIT
supported_coq_versions:
text: '8.16 or later'
opam: '{>= "8.16"}'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{>= "2.0"}'
description: |-
[MathComp ssreflect 2.0 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-algebra
description: |-
[MathComp algebra](https://math-comp.github.io)
tested_coq_opam_versions:
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.19'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.18'
repo: 'mathcomp/mathcomp-dev'
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.16'
repo: 'mathcomp/mathcomp'
namespace: gaia
keywords:
- name: Bourbaki
- name: set theory
- name: ordinal numbers
- name: cardinals
categories:
- name: Mathematics/Logic/Set theory
- name: Mathematics/Arithmetic and Number Theory/Number theory
documentation: |-
## Documentation
Gaia stands for: Geometry, Algebra, Informatics and Applications.
More information about the project is available at the [project website][gaia-url].
[gaia-url]: http://www-sop.inria.fr/marelle/gaia/
---