ssreflect 1.3pl2-1 source package in Ubuntu
Changelog
ssreflect (1.3pl2-1) unstable; urgency=low * New upstream release -- Ubuntu Archive Auto-Sync <email address hidden> Mon, 05 Dec 2011 11:04:28 +0000
Upload details
- Uploaded by:
- Ubuntu Archive Auto-Sync
- 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 |
---|
Downloads
File | Size | SHA-256 Checksum |
---|---|---|
ssreflect_1.3pl2.orig.tar.gz | 815.2 KiB | 9a3e10cbad61c307b1b1d4a80c17e39ad3d2c52d91dcab9292f3ef2bcc525339 |
ssreflect_1.3pl2-1.debian.tar.gz | 12.0 KiB | d5648bbb8a49a60c9dbf7ef7f81704a14c560fb5ae9fa3a248f298febcf01a01 |
ssreflect_1.3pl2-1.dsc | 2.2 KiB | abe5c71aaaa26b574305cfede9ad979ffa2b86ec8b131702f0a10ea56a9efe5a |
Available diffs
- diff from 1.3pl1-5build2 to 1.3pl2-1 (13.7 KiB)
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.