Опубликованный пакет / CLIR
arxo.order_composition
v0.1.0Совместная поддержка цепочки порядка правилами Lean и Isabelle
Пакет можно напечатать самостоятельным модулем на языке общего назначения, который отвечает без движка правил: ответ и статус, без доказательства, хэшей и канонического документа. Всё на этой странице взято из плана кодогенерации, построенного вместе с индексом; витрина ничего не вычисляет сама.
План кодогенерации
План строится: пакет печатается модулем.
- формат плана
- law-backend-plan/0.8
- возможности
- status:supported
Сверка сценариями пакета
совпало 7 из 7 сценариев на ts, py, go
- статусы ответов
- NEITHER 6 · TRUE_ONLY 1
Целевые языки
gopyts
отвергают этот план · 13
bslверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)csверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)dartверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)erlверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)exверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)javaверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)ktверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)luaверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)phpверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)rbверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)rsверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)scalaверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)swiftверсия плана не поддержана эмиттером: 'law-backend-plan/0.8' (поддержана law-backend-plan/0.7)
./law dev backend corpus/clir/arxo-order-composition.lawir.json --target ts --target py --target go --out DIR
arxo.orderisabelle.orderisabelle.order.permissionsmathlib.ordermathlib.order.permissions
Интерфейс модуля
Вопросы — публичные отношения с производящим правилом; входы — факты, которые вопрос читает. Имена функций следуют языку: ask_… в Python, ask.… в TypeScript, Ask… в Go.
Вопросы · 1
| Имя | Параметры | Смысл | Читает | Источники |
|---|---|---|---|---|
| jointly_supported_strict_chain | text, text, text, text, text | Jointly supported strict chain | in_carrierlinear_order_structurepartial_order_structurepreorder_structurepermit_3a9ac9ff49edf677c31208fa472a1dabde8eadb7e4581dd75c563e3687a9d1f4permit_50bc92ec5f62262e494bac475a39b971a5a1b5cff63d9236ecc3a9ba97fead88permit_cf7c23306a665bc0ff3fc08fffff0bd96bd3f400ad65990bf0a58da580b5d646permit_22aeb98e3dca72b4f5436967cb0eee630aabde47fd171b0942bac99c612760afpermit_7518ca9bf69a1dab886b841a3d0a1a8863349caf8a43819ce8fd0f39379bf690permit_c37e5578bf2e12f9752f6e310241b44b6743c7c058f83b4bdd23140f16287537permit_cb430046b1e38484a123fc047a67b89f9c0585a649a14e9095c3cdddee482831 | / |
Входы · 11
| Имя | Параметры | Смысл |
|---|---|---|
| in_carrier | text, text | Элемент принадлежит этому носителю |
| linear_order_structure | text | На носителе задан выбранный линейный порядок |
| partial_order_structure | text | На носителе задан выбранный частичный порядок |
| preorder_structure | text | На носителе задан выбранный предпорядок |
| permit_3a9ac9ff49edf677c31208fa472a1dabde8eadb7e4581dd75c563e3687a9d1f4 | Conditional permission: Orderings.preorder_class.less_imp_le | |
| permit_50bc92ec5f62262e494bac475a39b971a5a1b5cff63d9236ecc3a9ba97fead88 | Conditional permission: Orderings.preorder_class.less_trans | |
| permit_cf7c23306a665bc0ff3fc08fffff0bd96bd3f400ad65990bf0a58da580b5d646 | Conditional permission: Orderings.preorder_class.le_less_trans | |
| permit_22aeb98e3dca72b4f5436967cb0eee630aabde47fd171b0942bac99c612760af | Conditional permission: LinearOrder.toPartialOrder | |
| permit_7518ca9bf69a1dab886b841a3d0a1a8863349caf8a43819ce8fd0f39379bf690 | Conditional permission: le_of_lt | |
| permit_c37e5578bf2e12f9752f6e310241b44b6743c7c058f83b4bdd23140f16287537 | Conditional permission: le_trans | |
| permit_cb430046b1e38484a123fc047a67b89f9c0585a649a14e9095c3cdddee482831 | Conditional permission: PartialOrder.toPreorder |