-
Notifications
You must be signed in to change notification settings - Fork 1
/
coq-hanoi.opam
57 lines (48 loc) · 2.24 KB
/
coq-hanoi.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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
# 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: "[email protected]"
version: "dev"
homepage: "https://github.com/thery/hanoi"
dev-repo: "git+https://github.com/thery/hanoi.git"
bug-reports: "https://github.com/thery/hanoi/issues"
license: "MIT"
synopsis: "Hanoi tower in Coq"
description: """
Hanoi tower in Coq
| File | Content |
| --------------------------------- | -----------------------------------------|
| [extra](./extra.v) | Extra theorems from the standard library |
| [gdist](./gdist.v) | Distance in a graph |
| [ghanoi](./ghanoi.v) | General Hanoi framework |
| [ghanoi3](./ghanoi3.v) | General Hanoi framework with 3 pegs |
| [lhanoi3](./lhanoi3.v) | Linear Hanoi tower with 3 pegs |
| [rhanoi3](./rhanoi3.v) | Regular Hanoi tower with 3 pegs |
| [triangular](./triangular.v) | Theorems about triangular numbers |
| [phi](./phi.v) | Theorems about the Φ function |
| [psi](./psi.v) | Theorems about the Ψ function |
| [ghanoi4](./ghanoi4.v) | General Hanoi framework with 4 pegs |
| [rhanoi4](./rhanoi4.v) | Regular Hanoi tower with 4 pegs |
| [star](./star.v) | Some maths for the shanoi |
| [shanoi](./shanoi.v) | Hanoi tower in star |
| [shanoi4](./shanoi4.v) | Hanoi tower with 4 pegs in star |
A note about this development is available
[here](https://hal.inria.fr/hal-02903548).
An interactive version of the library is available
[here](https://thery.github.io/hanoi/index.html)."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {(>= "8.18")}
"coq-mathcomp-ssreflect" {(>= "2.1.0")}
"coq-mathcomp-algebra" {(>= "2.1.0")}
"coq-mathcomp-finmap" {(>= "2.0.0")}
"coq-mathcomp-bigenough" {(>= "1.0.1")}
]
tags: [
"keyword:hanoi tower"
"logpath:hanoi"
]
authors: [
"Laurent Théry"
]