Skip to content
docs
Arxo ↗

nb-23 solutions — Numbers and the standard library

For LLMs2 sections
← Back to lessonChapter 23 / 25 · Advanced II · Worked solution

Checkable against the standalone probe below (law engine test probe.lawtest --program probe.law: 2/2 pass) and, after adding the rule to the package, law test packs/examples/language-demo/numerics (67 + 2 checked, all passed). Tool law 0.1.0, language 0.2, semantics law.core/0.2, std 0.2.0. Identifiers and code as written.

Answer: the four-way split fires at 470 KZT; the three-way split carries INEXACT_DIVISION instead of a rounded amount.

1880 / 4 = 470 is exact, so late_quarter() == 470 KZT holds and the rule fires (TRUE_ONLY). 1880 / 3 is not 10-smooth, so the machine refuses the quiet rounding and the evaluation carries the coded INEXACT_DIVISION issue — the same discipline as section 5’s monthly/baddiv pair, at a different amount. Add to the package:

Arxo Law
pure function late_quarter() -> Money = 1880 KZT / 4.0;
pure function late_third() -> Money = 1880 KZT / 3.0;
relation late_ok() kind institutional;
rule LateOk strict {
when late_quarter() == 470 KZT;
then late_ok();
}

Two tests (append after the file header, standalone shape as in the article’s Standalone B):

Arxo Law
test "late quarter is exact" {
given {
context { legal_time @2026-03-02; decision_time @2026-03-02T09:00:00Z; knowledge_time @2026-03-02T09:00:00Z; timezone "UTC"; }
}
evaluate truth(late_ok());
expect truth_status == TRUE_ONLY;
}
test "late third is loud" {
given {
context { legal_time @2026-03-02; decision_time @2026-03-02T09:00:00Z; knowledge_time @2026-03-02T09:00:00Z; timezone "UTC"; }
}
evaluate late_third();
expect issue(INEXACT_DIVISION);
}

Verified 2026-10-03 as a standalone probe: test PASS: late quarter is exact, test PASS: late third is loud, lawc test: 2/2 тестов прошли. The divisor stays Decimal (/ 4, with an Integer divisor, is refused at check time with LDC-E2108); the mixed 1880 KZT + 10 EUR variant would stay NEITHER like the article’s mixed() rule and would NOT satisfy part (b), which asks for the loud issue, not silence.

Both probes refuse with the same two codes, exit 1: LDC-E2105 (name resolution — the term is neither in the file nor in the std v1-list) and LDC-E2403 (computability proof — without an effect descriptor for the callee, f cannot be proved PURE_DETERMINISTIC). Switching the ln2 probe’s return type to RealExpr adds a third diagnostic, LDC-E2101 at 4:17 (тип "RealExpr" не разрешается), while the two term codes stay: the type layer refuses independently of the term layer. Verified 2026-10-03: three error lines, exit 1. If you predicted the type change would remove a code, re-read §4 — each layer reports its own missing piece.

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.