File: coq-mathcomp-reals.opam

package info (click to toggle)
mathcomp-analysis 1.9.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 4,308 kB
  • sloc: sh: 420; python: 76; sed: 25; makefile: 7
file content (41 lines) | stat: -rw-r--r-- 1,022 bytes parent folder | download
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
opam-version: "2.0"
maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"
version: "dev"

homepage: "https://github.com/math-comp/analysis"
dev-repo: "git+https://github.com/math-comp/analysis.git"
bug-reports: "https://github.com/math-comp/analysis/issues"
license: "CECILL-C"

synopsis: "A library for real numbers for mathematical components"
description: """
This package contains a library for real numbers for
the Coq proof-assistant and using the Mathematical Components library."""

build: [make "-C" "reals" "-j%{jobs}%"]
install: [make "-C" "reals" "install"]
depends: [
  "coq-mathcomp-classical" { = version}
]

tags: [
  "category:Mathematics/Real Numbers"
  "keyword:real numbers"
  "keyword:reals"
  "keyword:extended real numbers"
  "logpath:mathcomp.reals"
]
authors: [
  "Reynald Affeldt"
  "Alessandro Bruni"
  "Yves Bertot"
  "Cyril Cohen"
  "Marie Kerjean"
  "Assia Mahboubi"
  "Damien Rouhling"
  "Pierre Roux"
  "Kazuhiko Sakaguchi"
  "Zachary Stone"
  "Pierre-Yves Strub"
  "Laurent Théry"
]