add coq-hol-light-real-with-N.1.2.0

Author: fblanqui

released/packages/coq-hol-light-real-with-N/coq-hol-light-real-with-N.1.2.0/opam

@@ -0,0 +1,30 @@
+opam-version: "2.0"
+synopsis: "Definition of HOL-Light real numbers in Coq using N"
+description: """
+This library provides a representation in Coq of the definition of real numbers
+in HOL-Light, using the Coq type N for natural numbers, automatically generated
+from HOL-Light using hol2dk and lambdapi.
+"""
+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: "[email protected]"
+authors: ["Frédéric Blanqui"]
+license: "CeCILL-2.1"
+depends: [
+  "coq" {>= "8.19"}
+]
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+tags: [
+  "logpath:HOLLight_Real_With_N"
+  "date:2025-02-19"
+  "category:Math/Arith/Misc"
+  "category:Math/Arith/Real numbers"
+  "keyword:HOL-Light"
+]
+url {
+  src: "https://github.com/Deducteam/coq-hol-light-real-with-N/archive/refs/tags/1.2.0.tar.gz"
+  checksum: "sha256=bfd5a1cd356b2208d4989d7024c694bf984816e85b479e8ec12319e75ab0c9bf"
+}