Package: wnpp Severity: wishlist Owner: Stephane Glondu <[EMAIL PROTECTED]>
* Package name : ssreflect Version : 1.1 Upstream Author : Georges Gonthier (Microsoft Research - Inria Joint Centre) * URL : http://www.msr-inria.inria.fr/Projects/math-components * License : CeCILL-B Programming Lang: OCaml, Coq Description : small scale reflection extension library for the Coq proof assistant 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). -- System Information: Debian Release: lenny/sid APT prefers testing APT policy: (990, 'testing'), (500, 'unstable'), (1, 'experimental') Architecture: i386 (i686) -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]