libcoq-mathcomp-real-closed (2.0.2-1build16)

Details

Core information at a glance

Distribution: ubuntu
Origin: ubuntu-stonking
Repository: https://ports.ubuntu.com
Codename: stonking
Component: universe
Source: mathcomp-real-closed
Architecture: riscv64
Section: universe/ocaml
Priority: optional
Maintainer: Ubuntu Developers <[email protected]>

Size & integrity

Byte sizes and integrity verification

Installed size: 10.3 kB
Size expected: 3 MB
Size actual: 3 MB
Size match

Dependencies

Required package dependencies

libcoq-mathcomp-algebra-msor3
libcoq-mathcomp-bigenough-3vkp6
libcoq-mathcomp-field-fz9y3
libcoq-mathcomp-ssreflect-s7137

Suggested packages

Recommended additional packages

ocaml-findlib

Description

Real closed fields for Mathematical Components

Homepage Download .deb

Checksums

Hash values and integrity verification status

Type	Expected	Actual
MD5	4cd030f4…88ee7983	4cd030f4…88ee7983
SHA-1	00b7aec1…cfd529bc	00b7aec1…cfd529bc
SHA-256	af4dd560…4818ebb6	af4dd560…4818ebb6
SHA-512	4a89063a…b5b5a8b8	4a89063a…b5b5a8b8

Files and directories included

.
usr
usr/lib
usr/lib/riscv64-linux-gnu
usr/lib/riscv64-linux-gnu/ocaml
usr/lib/riscv64-linux-gnu/ocaml/5.4.0
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/all_real_closed.glob
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/all_real_closed.v
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/all_real_closed.vo
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/cauchyreals.glob
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/cauchyreals.v
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/cauchyreals.vo
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/complex.glob
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/complex.v
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/complex.vo
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/mxtens.glob
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/mxtens.v
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/mxtens.vo
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/ordered_qelim.glob
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/ordered_qelim.v
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/ordered_qelim.vo
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/polyorder.glob
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/polyorder.v
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/polyorder.vo
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/polyrcf.glob
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/polyrcf.v
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/polyrcf.vo
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/qe_rcf.glob
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/qe_rcf.v
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/qe_rcf.vo
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/qe_rcf_th.glob
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/qe_rcf_th.v
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/qe_rcf_th.vo
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/realalg.glob
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/realalg.v
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq/user-contrib/mathcomp/real_closed/realalg.vo
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq-mathcomp-real-closed
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq-mathcomp-real-closed/META
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq-mathcomp-real-closed/dune-package
usr/lib/riscv64-linux-gnu/ocaml/5.4.0/coq-mathcomp-real-closed/opam
usr/share
usr/share/doc
usr/share/doc/libcoq-mathcomp-real-closed
usr/share/doc/libcoq-mathcomp-real-closed/README.md.gz
usr/share/doc/libcoq-mathcomp-real-closed/changelog.Debian.gz
usr/share/doc/libcoq-mathcomp-real-closed/copyright
var
var/lib
var/lib/coq
var/lib/coq/md5sums
var/lib/coq/md5sums/libcoq-mathcomp-real-closed.checksum