package coq-mathcomp-ssreflect

Overview
No Docs

You can search for identifiers within the package.

in-package search v0.2.0

Small Scale Reflection

Install

Dune Dependency

math-comp.github.io Edit opam file Versions (21)

Authors

Maintainers

M

Mathematical Components <mathcomp-dev@sympa.inria.fr>

Sources

mathcomp-1.10.0.tar.gz

sha256=3f8a88417f3456da05e2755ea0510c1bd3fd13b13c41e62fbaa3de06be040166

Description

This library includes the small scale reflection proof language extension and the minimal set of libraries to take advantage of it. This includes libraries on lists (seq), boolean and boolean predicates, natural numbers and types with decidable equality, finite types, finite sets, finite functions, finite graphs, basic arithmetics and prime numbers, big operators

Published: 02 Dec 2019

Dependencies (1)

coq (>= "8.7" & < "8.12~")

Dev Dependencies

None

Used by (24)

coq-ceramist
coq-comp-dec-modal < "1.1"
coq-coqeal-theory
coq-coquelicot >= "2.1.1"
coq-disel >= "2.1" & < "2.3"
coq-disel-examples < "2.3"
coq-extructures >= "0.2.2" & < "0.3.1"
coq-fcsl-pcm >= "1.1.1" & < "1.4.0"
coq-graph-theory < "0.9"
coq-hanoi
coq-interval < "4.11.1"
coq-lemma-overloading >= "8.10.0"
coq-mathcomp-bigenough
coq-mathcomp-dioid < "0.2"
coq-mathcomp-fingroup = "1.10.0"
coq-mathcomp-finmap >= "1.3.4" & < "1.5.0"
coq-mathcomp-multinomials >= "1.4" & < "1.5.2"
coq-mathcomp-odd-order = "1.10.0"
coq-msets-extra
coq-plouffe >= "1.2.0"
coq-quickchick >= "1.1.0"
coq-reglang >= "1.1" & < "1.1.3"
coq-vellvm
coq-wasm >= "2.0.1"

Conflicts