ssreflect 1.5~rc1-2 source package in Ubuntu
Changelog
ssreflect (1.5~rc1-2) unstable; urgency=low * Upload to unstable * Update Homepage -- Stéphane Glondu <email address hidden> Fri, 06 Dec 2013 08:28:06 +0100
Upload details
- Uploaded by:
- Debian OCaml Maintainers
- Uploaded to:
- Sid
- Original maintainer:
- Debian OCaml Maintainers
- Architectures:
- any all
- Section:
- math
- Urgency:
- Low Urgency
See full publishing history Publishing
| Series | Published | Component | Section |
|---|
Downloads
| File | Size | SHA-256 Checksum |
|---|---|---|
| ssreflect_1.5~rc1-2.dsc | 2.2 KiB | e163a9aec05463d705718e737241aee05ef320fc4105a39dbdf72fa77ee71baa |
| ssreflect_1.5~rc1.orig.tar.gz | 199.2 KiB | f85d8ced769b6c38a499681a52480f2e0b9b7a0a8f028a3d35ecd1794ae64fc2 |
| ssreflect_1.5~rc1-2.debian.tar.gz | 12.2 KiB | adac1360509c8424448b16890923a6e02c508772c322a710b26a0380f3b9f896 |
Available diffs
- diff from 1.4-2 to 1.5~rc1-2 (799.1 KiB)
No changes file available.
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: small scale reflection extension for Coq (plugin)
This package is part of Ssreflect, the small scale reflection
extension for Coq. It provides 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.
- libssreflect-ocaml-dev: small scale reflection extension for Coq (devt files)
This package is part of Ssreflect, the small scale reflection
extension for Coq. It provides the static native-code library, needed
to build custom toplevels, and the compiled interface.
