ssreflect 1.3pl2-2build1 source package in Ubuntu
Changelog
ssreflect (1.3pl2-2build1) precise; urgency=low * Rebuild against new Coq -- Andreas Moog <email address hidden> Sun, 08 Jan 2012 16:10:20 +0100
Upload details
- Uploaded by:
- Andreas Moog
- Uploaded to:
- Precise
- Original maintainer:
- Debian OCaml Maintainers
- Architectures:
- any all
- Section:
- math
- Urgency:
- Low Urgency
See full publishing history Publishing
Series | Published | Component | Section | |
---|---|---|---|---|
Precise | release | universe | math |
Downloads
File | Size | SHA-256 Checksum |
---|---|---|
ssreflect_1.3pl2.orig.tar.gz | 815.2 KiB | 9a3e10cbad61c307b1b1d4a80c17e39ad3d2c52d91dcab9292f3ef2bcc525339 |
ssreflect_1.3pl2-2build1.debian.tar.gz | 12.6 KiB | a6f40511936e452c05819f7720c8d97cb9938e8f5356f25c7f0304f0cbfd9c3a |
ssreflect_1.3pl2-2build1.dsc | 2.2 KiB | fee515af14b8c552b05c2a036c04f224378de2d800a3e27c3cf74dc3a7769f00 |
Available diffs
- diff from 1.3pl2-2 (in Debian) to 1.3pl2-2build1 (319 bytes)
Binary packages built by this source
- libssreflect-coq: small scale reflection library for Coq (theories)
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-oriented"
theories for basic combinatorics (roughly: arithmetic, lists, and
finite sets).
.
This package installs the full Ssreflect distribution.
- libssreflect-ocaml: No summary available for libssreflect-ocaml in ubuntu quantal.
No description available for libssreflect-ocaml in ubuntu quantal.
- libssreflect-ocaml-dev: No summary available for libssreflect-ocaml-dev in ubuntu quantal.
No description available for libssreflect-
ocaml-dev in ubuntu quantal.