« Up

matrix 1.0.6 2 m 0 s 🏆

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   8.18.0      The Coq Proof Assistant
coq-core              8.18.0      The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            8.18.0      The Coq Proof Assistant -- Standard Library
coqide-server         8.18.0      The Coq Proof Assistant, XML protocol server
dune                  3.13.0      Fast, portable, and opinionated build system
ocaml                 4.14.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.14.0      Official release 4.14.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.6       A library manager for OCaml
zarith                1.13        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
synopsis: "Formal matrix theory with multiple implementations in Coq" # One-line description
description: """
  Matrix is an important mathematical tool. Although there are at least five matrix 
  models/libraries in Coq community, the massive verification project involving matrix 
  are still facing some problems:
  (1). There havn't a full-feature formal matrix library, because the matrix theory is 
  complex and need more time to formalize it.
  (2). Different libraries of these implementations cannot be easily switched at the 
  later stage of a verification process, because the type of operations and theorems 
  are different. But some project maybe need more matrix theories while the needed 
  theorems only avaiable in another libraries.
  Thus, we provide a unified framework for different implementations of formal matrix
  models, so as to decouple the difference between underlying technologies and 
  upper-level applications.
""" # Longer description, can span several lines
homepage: "https://github.com/zhengpushi/CoqMatrix"
dev-repo: "git+https://github.com/zhengpushi/CoqMatrix.git"
bug-reports: "https://github.com/zhengpushi/CoqMatrix/issues"
doc: "https://zhengpushi.github.io/coq-matrix.html"
maintainer: "zhengpushi@nuaa.edu.cn"
authors: [
  "ZhengPu Shi"
]
license: "MIT" # Make sure this is reflected by a LICENSE file in your sources
depends: [
  "coq" {>= "8.18.0"}
]
build: [
  [make "-j%{jobs}%"]
]
install: [
  [make "install"]
]
  url {
  src: "https://github.com/zhengpushi/CoqMatrix/archive/refs/tags/1.0.6.tar.gz"
  checksum: "sha256=ea44c640a681900d2b81c1bc72c81a43cd02c29e78121042fd5cd6b00b9e171b"
}
tags: [
  "keyword:matrices"
  "category:Mathematics/Algebra"
  "date:2024-01-16"
  "logpath:CoqMatrix"
]

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-matrix.1.0.6 coq.8.18.0
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; timeout 4h opam install -y --deps-only coq-matrix.1.0.6 coq.8.18.0
Return code
0
Duration
1 m 0 s

Install 🚀

Command
opam list; echo; timeout 4h opam install -y -v coq-matrix.1.0.6 coq.8.18.0
Return code
0
Duration
2 m 0 s

Installation size

Total: 21 M

  • 948 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixNat.vo
  • 906 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorR.vo
  • 870 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorQ.vo
  • 867 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorC.vo
  • 866 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorQc.vo
  • 735 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixR.vo
  • 727 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixQ.vo
  • 723 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixC.vo
  • 717 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixQc.vo
  • 545 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorZ.vo
  • 497 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixAll.vo
  • 463 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/ListExt.vo
  • 416 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepList/Matrix.vo
  • 350 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorAll.vo
  • 350 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepList/Matrix.glob
  • 349 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/HierarchySetoid.vo
  • 346 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/SetoidListListExt.vo
  • 334 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixZ.vo
  • 320 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/ListExt.glob
  • 311 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepPair/Matrix.vo
  • 289 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/ElementType.vo
  • 288 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun/Matrix.vo
  • 252 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/SetoidListExt.vo
  • 246 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepPair/Matrix.glob
  • 245 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/SetoidListListExt.glob
  • 244 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Complex/Complex.vo
  • 233 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/Hierarchy.vo
  • 233 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepRec/MatrixTheoryDR.vo
  • 205 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Complex/Complex.glob
  • 198 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorNat.vo
  • 196 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun/Matrix.glob
  • 191 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepPair/Vector.vo
  • 188 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun2/vec.vo
  • 184 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepRec/Matrix.vo
  • 184 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/examples.vo
  • 177 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepRec/VectorTheoryDR.vo
  • 175 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepPair/VectorTheoryDP.vo
  • 172 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun2/vec.glob
  • 170 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/ElementType.glob
  • 165 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepRec/Matrix.glob
  • 164 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepList/VectorTheoryDL.vo
  • 155 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/SetoidListExt.glob
  • 154 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepList/MatrixTheoryDL.vo
  • 154 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/HierarchySetoid.glob
  • 148 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun/MatrixTheorySF.vo
  • 148 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Calculus/RealFunction.glob
  • 147 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/NatFun/VectorTheoryNF.vo
  • 143 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun2/MatrixTheorySF2.vo
  • 139 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepPair/Vector.glob
  • 138 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepPair/MatrixTheoryDP.vo
  • 136 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/NatFun/Matrix.vo
  • 134 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixHomo/MatrixHomomorphism.vo
  • 134 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixHomo/MatrixIsomorphism.vo
  • 127 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/RExt.vo
  • 122 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/Hierarchy.glob
  • 117 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/NatFun/Matrix.glob
  • 113 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/RExt.glob
  • 112 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepRec/MatrixTheoryDR.glob
  • 112 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/NatFun/MatrixTheoryNF.vo
  • 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/Sequence.vo
  • 91 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun/MatrixTheorySF.glob
  • 89 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun/Vector.vo
  • 89 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Calculus/RealFunction.vo
  • 86 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun2/MatrixTheorySF2.glob
  • 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixAll.glob
  • 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepList/Matrix.v
  • 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepList/MatrixTheoryDL.glob
  • 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/ListExt.v
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepPair/MatrixTheoryDP.glob
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/NatFun/MatrixTheoryNF.glob
  • 71 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixTheory.vo
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun/VectorTheorySF.vo
  • 68 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun/Vector.glob
  • 68 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/RAST.vo
  • 67 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun2/VectorTheorySF2.vo
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/BasicConfig.vo
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/SetoidListListExt.v
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/Sequence.glob
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepPair/Matrix.v
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorTheory.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Complex/Complex.v
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixTheory.glob
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Calculus/Derivative.glob
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/examples.glob
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Calculus/Derivative.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun/Matrix.v
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/LinearAlgebra/PermutationExt.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixHomo/HomomorphismThy.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/RExt.v
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/SetoidListExt.v
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/HierarchySetoid.v
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun/VectorTheorySF.glob
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepRec/VectorTheoryDR.glob
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepList/VectorTheoryDL.glob
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun2/VectorTheorySF2.glob
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/NatFun/VectorTheoryNF.glob
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/QcExt.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepPair/VectorTheoryDP.glob
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/NatExt.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/Hierarchy.v
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun2/vec.v
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepRec/Matrix.v
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorR.glob
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixHomo/IsomorphismThy.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepPair/Vector.v
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/ZExt.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/ElementType.v
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/LinearAlgebra/PermutationExt.glob
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Calculus/Calculus.vo
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/ExtrOcamlR.vo
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixAll.v
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Calculus/Integration.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/NatFun/Matrix.v
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/QExt.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Calculus/RealFunction.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/RAST.glob
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorTheory.glob
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/StrExt.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/MyExtrOCamlPArray.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepRec/MatrixTheoryDR.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun/MatrixTheorySF.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/BoolExt.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun2/MatrixTheorySF2.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixR.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/Sequence.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/NatExt.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun/Vector.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepPair/MatrixTheoryDP.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/FuncExt.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepList/MatrixTheoryDL.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/NatFun/MatrixTheoryNF.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorR.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixHomo/HomomorphismThy.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixHomo/IsomorphismThy.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixQ.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/BoolExt.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun2/VectorTheorySF2.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepList/VectorTheoryDL.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/SafeNatFun/VectorTheorySF.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixTheory.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/QExt.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/LinearAlgebra/PermutationExt.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorAll.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepPair/VectorTheoryDP.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/DepRec/VectorTheoryDR.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Calculus/Derivative.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/BasicConfig.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/NatFun/VectorTheoryNF.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/RAST.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/FuncExt.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/examples.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/BasicConfig.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixQ.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/StrExt.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorAll.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/NatExt.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixNat.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixZ.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixHomo/MatrixHomomorphism.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorTheory.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/QcExt.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixHomo/MatrixIsomorphism.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/QExt.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixHomo/HomomorphismThy.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixHomo/IsomorphismThy.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/ZExt.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorQ.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixR.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixZ.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/StrExt.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/FuncExt.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/TupleExt.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorQ.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/QcExt.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixHomo/MatrixIsomorphism.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixNat.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixC.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixQc.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorQc.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixHomo/MatrixHomomorphism.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixQc.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/BoolExt.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/MatrixC.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorC.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/CoqSetting.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorQc.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/ZExt.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorNat.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorZ.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorC.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/MyExtrOCamlPArray.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/ExtrOcamlR.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/TupleExt.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorNat.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/VectorZ.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/TupleExt.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Calculus/Integration.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/CoqSetting.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Calculus/Calculus.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Calculus/Calculus.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/MyExtrOCamlPArray.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/ExtrOcamlR.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/Calculus/Integration.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoqMatrix/CoqExt/CoqSetting.glob

Uninstall 🧹

Command
opam remove -y coq-matrix.1.0.6
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣