-
Notifications
You must be signed in to change notification settings - Fork 19
/
coq-fourcolor.opam
37 lines (32 loc) · 1.21 KB
/
coq-fourcolor.opam
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
# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.
opam-version: "2.0"
maintainer: "palmskog@gmail.com"
version: "dev"
homepage: "https://github.com/coq-community/fourcolor"
dev-repo: "git+https://github.com/coq-community/fourcolor.git"
bug-reports: "https://github.com/coq-community/fourcolor/issues"
license: "CECILL-B"
synopsis: "Mechanization of the Four Color Theorem in Coq"
description: """
This library contains a formal proof of the Four Color Theorem in Coq,
along with the theories needed to support stating and then proving the Theorem.
This includes an axiomatization of the setoid of classical real numbers,
basic plane topology definitions, and a theory of combinatorial hypermaps."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {(>= "8.16" & < "8.20~") | (= "dev")}
"coq-mathcomp-ssreflect" {(>= "2.0.0" & < "2.3~") | (= "dev")}
"coq-mathcomp-algebra"
]
tags: [
"category:Mathematics/Combinatorics and Graph Theory"
"keyword:Four color theorem"
"keyword:small scale reflection"
"keyword:Mathematical Components"
"logpath:fourcolor"
]
authors: [
"Georges Gonthier"
]