Pakiet: libssreflect-coq (1.6.1-3build1)
Odnośniki dla libssreflect-coq
Zasoby systemu Trisquel:
- Install using apturl
- Entry at directory.fsf.org
- Raporty o błędach
- Changelog
- Informacje nt. praw autorskich
Pobieranie pakietu źródłowego ssreflect:
Opiekun:
Original Maintainers:
- Debian OCaml Maintainers (Archiwum e-mail)
- Stéphane Glondu
- Enrico Tassi
Zasoby zewnętrzne:
- Strona internetowa [math-comp.github.io]
Podobne pakiety:
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 comprehensive set of Coq libraries covering topics as combinatorics
and algebra.
This package installs the full Ssreflect distribution.
Inne pakiety związane z libssreflect-coq
|
|
|
-
- dep: coq-8.6+4.05.0
- pakiet wirtualny udostępniany przez coq
-
- dep: libssreflect-ocaml (>= 1.6.1-3build1)
- small scale reflection extension for Coq (plugin)
Pobieranie libssreflect-coq
Architektura | Rozmiar pakietu | Rozmiar po instalacji | Pliki |
---|---|---|---|
all | 23 632,8 KiB | 138793 KiB | [lista plików] |