všetky možnosti
squeeze  ] [  wheezy  ] [  jessie  ] [  stretch  ] [  sid  ]
[ Zdroj: ssreflect  ]

Balík: libssreflect-coq (1.2+dfsg-6)

Odkazy pre libssreflect-coq


Zdroje Debian:

Stiahnuť zdrojový balík ssreflect:


Externé zdroje:

Podobné balíky:

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 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.

Ostatné balíky súvisiace s balíkom libssreflect-coq

  • závisí
  • odporúča
  • navrhuje
  • enhances

Stiahnuť libssreflect-coq

Stiahnuť pre všetky dostupné architektúry
Architektúra Veľkosť balíka Nainštalovaná veľkosť Súbory
all 3,576.0 kB14,312.0 kB [zoznam súborov]