File tree Expand file tree Collapse file tree 3 files changed +11
-1
lines changed Expand file tree Collapse file tree 3 files changed +11
-1
lines changed Original file line number Diff line number Diff line change @@ -19,6 +19,6 @@ opam install coq coq-interval
19
19
```
20
20
Run ` make ` to compile the proofs. We have tested compilation with Coq versions 8.10.1-8.16.1 and Interval versions 4.0.0-4.6.1.
21
21
22
- To use this repository as a library, run ` opam pin coq-euler htts ://github.com/taorunz/euler.git ` .
22
+ To use this repository as a library, run ` opam pin coq-euler https ://github.com/taorunz/euler.git ` .
23
23
Then, to import files into your Coq project, use ` Require Import euler.FILENAME ` .
24
24
Subsequent updates can be pulled using ` opam install coq-euler ` .
Original file line number Diff line number Diff line change @@ -6,6 +6,10 @@ description: """
6
6
Coq proof for the asymptotic upper bound of the
7
7
Euler Totient Function φ
8
8
"""
9
+ maintainer: ["@taorunz"]
10
+ authors: ["Runzhou Tao and Yuxiang Peng"]
11
+ homepage: "https://github.com/taorunz/euler"
12
+ bug-reports: "https://github.com/taorunz/euler/issues"
9
13
depends: [
10
14
"dune" {>= "2.8"}
11
15
"coq-interval" {>= "4.0.0"}
@@ -26,3 +30,4 @@ build: [
26
30
"@doc" {with-doc}
27
31
]
28
32
]
33
+ dev-repo: "git+https://github.com/taorunz/euler.git"
Original file line number Diff line number Diff line change 1
1
(lang dune 2 .8)
2
+ (name coq-euler)
2
3
( version 1 .0.0)
3
4
(using coq 0 .2)
4
5
5
6
( generate_opam_files true )
6
7
8
+ ( authors " Runzhou Tao and Yuxiang Peng" )
9
+ ( maintainers " @taorunz" )
10
+ ( source ( github taorunz/euler) )
11
+
7
12
( package
8
13
(name coq-euler)
9
14
(synopsis " Asymptotic lower bound of the Euler Totient Function" )
You can’t perform that action at this time.
0 commit comments