libssreflect-coq binary package in Ubuntu Precise powerpc
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 set of Coq libraries that provide core "reflection-
theories for basic combinatorics (roughly: arithmetic, lists, and
finite sets).
.
This package installs the full Ssreflect distribution.
Publishing history
Date | Status | Target | Component | Section | Priority | Phased updates | Version | ||
---|---|---|---|---|---|---|---|---|---|
2012-01-08 16:03:32 UTC | Published | Ubuntu Precise powerpc | release | universe | math | Extra | 1.3pl2-2build1 | ||
|
|||||||||
2012-01-08 16:04:27 UTC | Superseded | Ubuntu Precise powerpc | release | universe | math | Extra | 1.3pl2-2 | ||
|
|||||||||
2012-01-09 00:34:20 UTC | Superseded | Ubuntu Precise powerpc | release | universe | math | Extra | 1.3pl2-1 | ||
|
|||||||||
2011-12-06 08:05:33 UTC | Superseded | Ubuntu Precise powerpc | release | universe | math | Extra | 1.3pl1-5build2 | ||
|
|||||||||
2011-11-19 19:05:07 UTC | Superseded | Ubuntu Precise powerpc | release | universe | math | Extra | 1.3pl1-5build1 | ||
|
|||||||||
2011-11-13 05:04:54 UTC | Superseded | Ubuntu Precise powerpc | release | universe | math | Extra | 1.3pl1-4build1 | ||
|