coq-hol-light-real-with-N/opam at main · agontard/coq-hol-light-real-with-N · GitHub

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
opam-version: "2.0"
synopsis: "HOL-Light definition of real numbers using N"
description: """
This library contains an automatic translation of the HOL-Light
definition of real numbers using https://github.com/Deducteam/hol2dk
with the HOL-Light type of natural numbers mapped to the Rocq type N.
"""
homepage: "https://github.com/Deducteam/coq-hol-light-real-with-N"
dev-repo: "git+https://github.com/Deducteam/coq-hol-light-real-with-N.git"
bug-reports: "https://github.com/Deducteam/coq-hol-light-real-with-N/issues"
doc: "https://github.com/Deducteam/coq-hol-light-real-with-N"
maintainer: "frederic.blanqui@inria.fr"
authors: ["https://github.com/Deducteam/coq-hol-light-real-with-N/blob/main/AUTHORS.md"]
license: "CeCILL-2.1"
depends: [
  "rocq-prover" {>= "9.0"}
]
build: [make "-j%{jobs}%"]
install: [make "install"]
tags: [
  "logpath:HOLLight_Real_With_N"
  "date:2025-07-11"
  "category:Mathematics/Arithmetic and Number Theory/Miscellaneous"
  "category:Mathematics/Real Numbers"
  "keyword:HOL-Light"
]