forked from coq-community/bertrand
-
Notifications
You must be signed in to change notification settings - Fork 0
/
coq-knuth-prime.opam
33 lines (29 loc) · 1 KB
/
coq-knuth-prime.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
opam-version: "2.0"
maintainer: "palmskog@gmail.com"
version: "dev"
homepage: "https://github.com/coq-community/bertrand"
dev-repo: "git+https://github.com/coq-community/bertrand.git"
bug-reports: "https://github.com/coq-community/bertrand/issues"
license: "LGPL-2.1-or-later"
synopsis: "Correctness of a WhyML implementation of Knuth's algorithm for prime numbers"
description: """
A proof of correctness of a WhyML implementation of the algorithm
for computing prime numbers as described in "The Art of Computer Programming:
Fundamental Algorithms" by Knuth, pp. 147-149."""
build: [make "why"]
depends: [
"coq" {= "8.12.1"}
"why3" {= "1.3.3"}
"why3-coq" {= "1.3.3"}
"alt-ergo" {= "2.3.3"}
"coq-bertrand" {= version}
]
tags: [
"category:Mathematics/Arithmetic and Number Theory/Number theory"
"category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs based on external tools"
"keyword:Knuth's algorithm"
"keyword:Bertrand's postulate"
]
authors: [
"Laurent Théry"
]