forked from coq-community/hydra-battles
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcoq-addition-chains.opam
33 lines (29 loc) · 1.03 KB
/
coq-addition-chains.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/hydra-battles"
dev-repo: "git+https://github.com/coq-community/hydra-battles.git"
bug-reports: "https://github.com/coq-community/hydra-battles/issues"
license: "MIT"
synopsis: "Exponentiation algorithms following addition chains"
description: """
Addition chains are algorithms for computations of the p-th power of some x,
with the least number of multiplication as possible. We present a few implementations of addition chains, with proofs of their correctness"""
build: ["dune" "build" "-p" name "-j" jobs]
depends: [
"dune" {>= "2.5"}
"coq" {(>= "8.13" & < "8.14~") | (= "dev")}
"coq-paramcoq" {(>= "1.1.2" & < "1.2~") | (= "dev")}
"coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.13~") | (= "dev")}
"coq-mathcomp-algebra"
]
tags: [
"category:Mathematics/Combinatorics and Graph Theory"
"keyword:addition chains"
"keyword:exponentiation algorithms"
"logpath:additions"
]
authors: [
"Pierre Castéran"
"Yves Bertot"
]