Источник / закреплённая редакция
rocq
Источник пакета rocq.order · 9.2
- work
- urn:arxo:rocq.order#Import_Source_6ed19e2eff811757d626083656cd1ce8132c17ab1851fd314c8496f5b2f79df0
- номер
- 9.2
- вид
- urn:arxo:rocq.order#treatise
Import_Edition_6ed19e2eff811757d626083656cd1ce8132c17ab1851fd314c8496f5b2f79df0
- edition
- urn:arxo:rocq.order#Import_Edition_6ed19e2eff811757d626083656cd1ce8132c17ab1851fd314c8496f5b2f79df0
- язык
- en
- официальность
- official
- материализация
- PINNED_OFFICIAL_BYTES
- жизненный цикл
- —
Публикации
| URI | Тип | documentHash | Получено |
|---|---|---|---|
| https://github.com/rocq-prover/stdlib/blob/V9.2.0/theories/QArith/QArith_base.v | text/plain; charset=utf-8 | sha256:d9108f8e6f33e8854da3525c0a41faaa4915ae4dee80a906891962fb65764aa3 | 2026-09-12T20:15:36Z |
Фрагменты — 3
Stdlib.QArith.QArith_base.Qlt_trans · lemma · на него ссылаются: 1
en · official · sha256:6f27f9698ef82440cc3e6eb4510f7a29e6ef7bef9bccd364ae97e7a01fea2c0bEN
Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z.Ссылаются нормы: Import_Rule_8872a36d422eacd990d2e74a5dc1e191ea3ec7a256f3b7316d1ac7bf9c7121c7
Stdlib.QArith.QArith_base.Qlt_le_weak · lemma · на него ссылаются: 1
en · official · sha256:1731977af5e2421304d222dfefcc9dbdd6c3bc819e169062ec984222f0b01ea8EN
Lemma Qlt_le_weak x y : x<y -> x<=y.Ссылаются нормы: Import_Rule_c19ccc16514506ba5e9b2d9ffae5559844a67b72b2027eb3b225008346c18387
Stdlib.QArith.QArith_base.Qle_lt_trans · lemma · на него ссылаются: 1
en · official · sha256:02ce79602f950be5928e29c546301735a6a242fe740669570df42c5b7cc83ca7EN
Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z.Ссылаются нормы: Import_Rule_ffcef37c25169dbe372b14baf1a8bf6f49b69f80e6aa33f3274414942b069a10
Хэш рядом с текстом — sha256 его точных байтов. Он и есть проверка того, что показанный текст совпадает с закреплённым в пакете: расхождение роняет статику оракула.