» Ubuntu » Packages » lucid (10.04LTS) » math » libssreflect-coq
lucid  ] [  precise  ] [  raring  ] [  saucy  ] [  trusty  ] [  utopic  ]
[ Source: ssreflect  ]

Package: libssreflect-coq (1.2+dfsg-3build1) [universe]

Links for libssreflect-coq

Screenshot

Ubuntu Resources:

Download Source Package ssreflect:

Maintainer:

Please consider filing a bug or asking a question via Launchpad before contacting the maintainer directly.

Original Maintainers (usually from Debian):

It should generally not be necessary for users to contact the original maintainer.

External Resources:

Similar packages:

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.

Other Packages Related to libssreflect-coq

  • depends
  • recommends
  • suggests

Download libssreflect-coq

Download for all available architectures
Architecture Package Size Installed Size Files
all 3,575.9 kB14,316.0 kB [list of files]