libssreflect-coq 1.6.1-3build1 (amd64 binary) in ubuntu eoan
The name Ssreflect stands for "small scale reflection", a style of
proof that evolved from the computer-checked proof of the Four Colour
Theorem and which leverages the higher-order nature of Coq's
underlying logic to provide effective automation for many small,
clerical proof steps. This is often accomplished by restating
("reflecting") problems in a more concrete form, hence the name. For
example, in the Ssreflect library, arithmetic comparison is not an
abstract predicate, but a function computing a boolean.
.
The Ssreflect distribution comprises two parts:
* A new tactic language, which promotes more structured, concise and
robust proof scripts, and is in fact independent from the "reflection"
proof style. It is implemented as a linkable extension to the Coq
system.
* A comprehensive set of Coq libraries covering topics as combinatorics
and algebra.
.
This package installs the full Ssreflect distribution.
Details
- Package version:
- 1.6.1-3build1
- Status:
- Superseded
- Component:
- universe
- Priority:
- Optional
Downloadable files
- libssreflect-coq_1.6.1-3build1_all.deb (23.1 MiB)
Package relationships
- Depends on:
- coq-8.6+4.05.0
- libssreflect-ocaml (>= 1.6.1-3build1)
- Provides:
- libmathcomp-coq
- ssreflect