Debian logoDebian Screenshots >


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
* A comprehensive set of Coq libraries covering topics as combinatorics
  and algebra.

This package installs the full Ssreflect distribution.

Upload more screenshots

Please help extend the collection of screenshots. Just make a screenshot and upload it here. You don't need to register or anything.



49 other people were interested in this package here. The newest known version of this software is 1.6-1 (Information last updated 4 days ago.)