Cheat sheet

For LLMs19 sections

The whole language on one page. Every law block below belongs to one package: put them together in parking.law and it compiles; the scenarios at the end run against it. Each section links to the page that explains the construct in depth.

Open this package in the playground → — edit the rules and the scenarios of this page and run them in your browser.

Package header

language "law.core" version "0.2";
package demo.parking version "0.1.0";
namespace "urn:law:demo:parking";

Three lines open every package: the language version, the package name and version, and the namespace that makes every name globally unique.

Vocabulary

entity Applicant;
entity Office;

enum Zone {
    central;
    outer;
}

relation resident(a: Applicant) kind institutional;
relation vehicle_registered(a: Applicant) kind institutional;
relation permit_eligible(a: Applicant) kind institutional;
relation permit_suspended(a: Applicant) kind institutional;
relation outstanding_fines(a: Applicant) kind institutional;
relation disability_badge(a: Applicant) kind institutional;
relation fraud_flag(a: Applicant) kind institutional;
relation household_member(a: Applicant, m: Applicant) kind empirical;
relation large_household(a: Applicant) kind institutional;
relation lives_in(a: Applicant, z: Zone) kind empirical;
relation application_filed(a: Applicant, on: Date) kind empirical { key(a); }
relation decision_due(a: Applicant, due: Date) kind institutional;
relation decision_notified(a: Applicant) kind empirical;
relation resells_permit(a: Applicant) kind empirical;
relation revocation_notice(o: Office, a: Applicant) kind empirical;
relation permit_revoked(a: Applicant) kind institutional;
relation permit_office(o: Office) kind institutional;

Form	Meaning
`entity Name;`	a kind of thing the norm talks about
`enum Name { a; b; }`	a closed list of values
`relation name(x: Type, …) kind …;`	a statement that can be true, false, both or unknown
`kind institutional`	true because a rule or an authority says so
`kind empirical`	true because it happened; comes from evidence
`{ key(a); }`	at most one record per key: a second value is a conflict

Values

const MONTHLY_RATE: Money = 10 EUR;
const LARGE_HOUSEHOLD: Integer = 4;

function permit_fee(months: Integer) -> Money = months * MONTHLY_RATE;

Constants and pure functions. Money carries its currency (10 EUR), percentages are written 25 percent, dates @2026-03-01, periods 30 calendar_day.

Rules

rule PermitEligibility defeasible {
    for a: Applicant;
    when resident(a) and vehicle_registered(a);
    then permit_eligible(a);
    unless permit_suspended(a);
}

Strength	When to use it
`strict`	no exception is possible; `unless` on it is an error (`LDC-E4110`)
`defeasible`	the general rule that exceptions may defeat
`defeater`	an exception that withdraws a conclusion without asserting the opposite

for binds variables, when is the condition, then the conclusion, unless a proviso that blocks this rule only. A conclusion not p(x) is a refusal: it supports the opposite. See Your first rule and Exceptions and priorities.

Exceptions and priority

rule FinesRefusal defeasible {
    for a: Applicant;
    when outstanding_fines(a);
    then not permit_eligible(a);
}

rule BadgeEligibility defeasible {
    for a: Applicant;
    when disability_badge(a);
    then permit_eligible(a);
}

priority RefusalOverEligibility {
    prefer FinesRefusal over PermitEligibility;
    reason lex_specialis;
}

rule FraudBlocksBadge defeater {
    for a: Applicant;
    when fraud_flag(a);
    defeat permit_eligible(a);
}

You want	Write
an exception inside one rule	`unless …;`
a refusal	a rule with `then not p(x);`
one rule to beat another	`priority … { prefer A over B; reason …; }`
to cancel support without refusing	a `defeater` rule with `defeat p(x);`

Two rules with opposite conclusions and no priority give BOTH: the conflict is reported, not silently resolved.

Definitions, negation, aggregates

definition central_resident(a: Applicant) exact {
    when resident(a) and lives_in(a, central);
}

rule LargeHousehold strict {
    for a: Applicant;
    when resident(a)
        and count(collect m: Applicant where household_member(a, m)) >= LARGE_HOUSEHOLD;
    then large_household(a);
}

In a condition	Means
`p(x)`	`p(x)` is established
`not p(x)`	the opposite of `p(x)` is established
`not_known(p(x))`	nothing establishes `p(x)`
`count(collect m: T where …)`	how many values satisfy the condition
`sum(collect all v: Money, m: T where …)`	the total of the values

definition names a concept (“who counts as …”); the explanation then says “by definition”. Missing and refuted facts are different answers — see Missing and conflicting facts.

Closed lists

relation applicant_on_file(a: Applicant) kind institutional;

closure ResidentsRegister {
    predicate resident;
    domain applicant_on_file;
    snapshot "urn:snapshot:demo-parking-residents:2026";
    complete_as_of @2026-01-01T00:00:00Z;
    derive_explicit_negative true;
}

By default silence proves nothing: a missing record gives NEITHER. A closure says the register is complete for a domain at a moment, so inside that domain a missing record becomes a denial (FALSE_ONLY); outside it, silence stays silence.

Time and deadlines

deadline policy CALENDAR_DAYS {
    start_count next_day;
    include_end true;
    roll no_roll;
}

rule DecisionDeadline strict {
    for a: Applicant;
    for on: Date;
    when application_filed(a, on);
    then decision_due(a, add_calendar_period(on, 30 calendar_day));
}

Form	Meaning
`add_calendar_period(d, 30 calendar_day)`	calendar arithmetic; needs a deadline policy in the case
`add_business_days(d, n)`	working days; also needs the official calendar
`effective [@2026-01-01, infinity);`	inside a rule: when the rule is in force
`deadline policy … { … }`	how to count: start, end, rolling over holidays

Without a policy the deadline is not guessed: the answer is MISSING_POLICY. See Sources and legal time.

Sources and editions

source PARKING_RULES {
    kind municipal_act;
    jurisdiction NORTHBRIDGE;
    number "2026-1";
    label en official "Northbridge Residential Parking Rules";
}

edition PARKING_RULES_2026 of PARKING_RULES {
    language en;
    officiality official;
    adopted @2025-12-01;
    in_force [@2026-01-01, infinity);
    materialization_status PINNED_OFFICIAL_BYTES;
}

publication PARKING_RULES_2026_TEXT of PARKING_RULES_2026 {
    media_type "text/plain; charset=utf-8";
    uri "urn:demo:parking:rules:2026";
    retrieved_at @2026-01-05T09:00:00Z;
    content_hash "sha256:9060e85e1fd30cd22b8a9f618afb8aabd15ae356b23b47f86ab1689b6aacb660";
    local_path "sources/parking-rules-2026.txt";
}

fragment PARKING_RULES_2026_ART2 in PARKING_RULES_2026 {
    kind article;
    locator "article/2";
    label en official "Article 2. Eligibility";
    text en official """A residential parking permit is issued to an applicant who is a resident of Northbridge and has a vehicle registered at their address.
""";
    content_hash "sha256:e309c8a75c1eab992dd0ad66ff477f9111bf99651e167ce1de6a651129a758be";
}

relation eligibility_notice(a: Applicant) kind institutional;

@source(PARKING_RULES_2026_ART2)
rule EligibilityNotice defeasible {
    effective [@2026-01-01, infinity);
    for a: Applicant;
    when permit_eligible(a);
    then eligibility_notice(a);
}

Form	Meaning
`source`	the act itself: kind, jurisdiction, number
`edition … of …`	one version of the act, with its dates in force
`publication … of …`	the official bytes of an edition, pinned by hash
`fragment … in …`	an article or clause, with its text and hash
`@source(FRAGMENT)`	anchors a rule to the text it formalizes
`effective [from, to);`	when the rule applies; outside it the rule does not fire

The answer cites the fragment, and the hash proves which text was used. See Sources and legal time.

Duties, prohibitions, powers

rule DecisionDuty strict {
    for a: Applicant;
    for o: Office;
    for on, due: Date;
    when application_filed(a, on) and decision_due(a, due) and permit_office(o);
    then duty NotifyDecision {
        bearer o;
        beneficiary a;
        goal achievement {
            condition decision_notified(a);
            window [on, due];
        }
    };
}

rule NoResale strict {
    for a: Applicant;
    for o: Office;
    when permit_eligible(a) and permit_office(o);
    then prohibition NoPermitResale {
        bearer a;
        beneficiary o;
        action resells_permit(a);
        window [@2026-01-01, @2026-12-31];
    };
}

rule RevocationPower strict {
    for a: Applicant;
    for o: Office;
    when permit_office(o) and permit_eligible(a);
    then power RevokePermit {
        holder o;
        over a;
        exercise revocation_notice(o, a);
        valid_when (resells_permit(a));
        effect create(permit_revoked(a));
    };
}

Position	Says	Key fields
`duty`	the bearer must bring something about	`bearer`, `beneficiary`, `goal`, `window`
`prohibition`	the bearer must not do something	`bearer`, `action`, `window`
`power`	the holder can change the legal situation	`holder`, `over`, `exercise`, `valid_when`, `effect`

The engine reports each position’s state: ACTIVE, FULFILLED, VIOLATED and others, with the facts behind it.

Packages and imports

pub relation permit_holder(a: Applicant) kind institutional;

Only declarations marked pub are visible to other packages. A package that uses another one names it in law.toml and imports it; foreign names are written with the package prefix. These lines are not part of this page’s package:

[dependencies]
"demo.parking" = "0.1.0"

import demo.parking version "0.1.0";

rule ResidentDiscount strict {
    for a: demo.parking::Applicant;
    when demo.parking::permit_holder(a);
    then discount(a);
}

law add demo.parking@0.1.0 writes the dependency and the lock for you. Referring to a name that is not pub fails with LDC-E1105.

Asking questions

Questions are asked in a scenario (.lawtest) or with law ask.

Question	Form	Answer
is it true?	`evaluate truth(p(x));`	a truth status
who?	`evaluate collect a: Applicant where p(a);`	a list
how much?	`evaluate permit_fee(3);`	a value
when?	`evaluate truth(decision_due(x, @2026-04-02));`	a truth status for the date
who owes what?	`evaluate positions();`	positions and their states

Four answers

Status	Means
`TRUE_ONLY`	established, nothing against
`FALSE_ONLY`	refuted, nothing for
`BOTH`	grounds on both sides: a conflict the package does not resolve
`NEITHER`	not established, not refuted: something is missing

Next to the truth status every answer carries an evaluation_status: COMPUTED when the engine had everything it needed, or a reason such as MISSING_POLICY when it did not.

Scenarios

test "the general rule" {
    given {
        context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
        assert resident(entity_ref("urn:demo:parking:ann")) { id "resident-ann"; origin case_input; }
        assert vehicle_registered(entity_ref("urn:demo:parking:ann")) { id "vehicle_registered-ann"; origin case_input; }
    }
    evaluate truth(permit_eligible(entity_ref("urn:demo:parking:ann")));
    expect truth_status == TRUE_ONLY;
    expect applied(PermitEligibility);
}

Part	Holds
`context { … }`	legal time, decision time, knowledge time, timezone, deadline policy
`assert p(x) { id "…"; origin case_input; }`	one fact with its identity and origin
`assert not p(x) { … }`	a stated denial
`evaluate …;`	the question
`expect …;`	`truth_status ==`, `evaluation_status ==`, `applied(Rule)`, `value ==`, `collected(…)`, `position(Name, STATE)`

Commands

law init my-package
law engine check parking.law
law engine test tests/scenarios.lawtest --program parking.law
law engine fmt parking.law
law ask my-case --query 'evaluate truth(permit_eligible(entity_ref("urn:demo:parking:ann")));' --query-id q1
law explain LDC-E4110
law codegen demo.parking --target ts --out gen --name parking --version 0.1.0

Command	Does
`law init`	a new package or case
`law engine check`	compile and report diagnostics
`law engine test`	run scenarios against the package
`law engine fmt`	format the source
`law ask`	ask a question of a case; the answer comes with its proof and hashes
`law explain LDC-E…`	what a diagnostic means and how to fix it
`law codegen`	a TypeScript, Python or Go module of the package, no engine needed

Common errors

Each row is checked: the page is changed as described, and the compiler must report exactly this code.

Code	Cause	Fix
`LDC-E0201`	a missing `;` or rule strength	end declarations and clauses with `;`; specify the rule strength
`LDC-E0203`	a keyword used as a name (`entity rule;`)	pick another name
`LDC-E1201`	the same name declared twice	rename one of them
`LDC-E1305`	a duty without `bearer`	name who owes the duty
`LDC-E1308` (warning)	`defeat` in a non-defeater rule	make the rule a `defeater`
`LDC-E1330`	a name in the conclusion that nothing binds	bind it with `for` and use it in `when`
`LDC-E2101`	an unknown type	declare it with `entity`, `enum` or `type`
`LDC-E2102`	a relation that is not declared	declare it, or fix the spelling
`LDC-E2103`	wrong number of arguments	match the declaration
`LDC-E4101`	a variable bound only under `not`	bind it by a positive condition first
`LDC-E4108`	a priority names a rule that does not exist	fix the rule name
`LDC-E4110`	`unless` on a `strict` rule	make the rule `defeasible`

law explain LDC-E… prints the full card for any code.

Types

Type	What it holds
`Algebraic`	An exact algebraic real number: a minimal polynomial plus the index of its real root.
`Boolean`	A two-valued data type: `true` or `false`.
`Bounds`	A closed rational interval bundled with the derivation that produced it.
`Currency`	The currency of a `Money` amount — the code in a literal such as `1000000 KZT`.
`Date`	A calendar date, written as `@2008-03-01`.
`Decimal`	An exact decimal number, written as a literal such as `0.20`.
`Duration`	A physical duration in seconds and nanoseconds.
`Instant`	A point on the time axis, written with an offset: `@2026-03-31T18:00:00+05:00`.
`Integer`	A whole number.
`Jurisdiction`	The type of a jurisdictional binding: a code that names a legal order.
`LanguageTag`	A BCP-47 language tag such as `kk-KZ`.
`List`	An ordered collection that allows duplicates.
`Magnitude`	A value whose dimension is computed from the unit registry, with product, quotient and conversion.
`Money`	An amount in a named currency, written as a literal such as `1000000 KZT`.
`Number`	The single exact numeric domain of 0.4 programs: every numeric spelling is one value, carried as an irreducible fraction.
`Option`	An optional value: there is no `null`, absence is `Option<T>`.
`Quantity`	A number with a unit tag, written as a literal such as `300 km`.
`Rational`	An exact rational value: the result type of exact division, serialized as an irreducible fraction.
`RealExpr`	A symbolic real expression over exact leaves and named constants such as `pi()` and `ln2()`.
`Set`	An unordered collection without duplicates.
`Text`	A text value; text is NFC-normalized.
`Timezone`	An IANA time zone name such as `Asia/Qyzylorda`.

Standard library

Function	What it does
`add_business_days(after, count)`	Steps a date by counted days under the calendar snapshot and the deadline policy.
`add_calendar_period(after, count)`	Steps a date by a calendar period: days, weeks, months or years.
`add_duration(after, duration)`	The instant that lies a physical duration after `after`.
`add_legal_term(date, term)`	Steps a date by a legal term, choosing the operation by the unit of the term.
`angle_convert(value, from, to, policy)`	Exact angle conversion under an explicit versioned policy.
`bounds_add(a, b)`	Interval sum: `[a.lo + b.lo, a.hi + b.hi]`.
`bounds_const(num, den)`	The degenerate interval `[f, f]` for the exact number `f = num/den`.
`bounds_div(a, b)`	Interval quotient of two bounds.
`bounds_mul(a, b)`	Interval product of two bounds.
`bounds_scale(b, num, den)`	Multiplies an interval by the exact factor `num/den`.
`bounds_sub(a, b)`	Interval difference: `[a.lo - b.hi, a.hi - b.lo]`.
`convert(value, num, den, unit)`	Converts a `Quantity` to another unit by the exact factor `num/den`.
`cos_bounds(x, profile)`	Certified bounds of the cosine of `x`.
`count(xs)`	Counts the elements of a collection; an empty collection gives 0.
`days_between(from, to)`	Number of calendar days from `from` to `to`; negative when `to` precedes `from`.
`div_round(dividend, divisor, precision, mode)`	Divides and rounds the exact quotient to a precision under a named mode.
`exact_sqrt(value)`	Exact square root of a rational argument; takes no precision profile.
`exp_bounds(x, profile)`	Certified bounds of `e` to the power `x`, for any sign of `x`.
`hours_between(from, to)`	Number of full hours between two instants; negative when the order is reversed.
`ln_bounds(x, profile)`	Certified bounds of the natural logarithm of `x`.
`ln2()`	The constant ln 2 as an exact symbolic value, without rounding.
`magnitude(q)`	Lifts a `Quantity` into the dimension algebra as a `Magnitude`.
`max(xs)`	The largest value of a collection.
`min(xs)`	The smallest value of a collection.
`minutes_between(from, to)`	Number of full minutes between two instants, with the sign and truncation of `hours_between`.
`month_end_of(d)`	The last day of the month containing the date.
`month_start_of(d)`	The first day of the month containing the date.
`pi()`	The constant π as an exact symbolic value, without rounding.
`pi_bounds(profile)`	Certified bounds of π at the precision of a profile.
`quantity_of(m, unit)`	Turns a `Magnitude` back into a `Quantity` of the named unit.
`round(value, precision, mode)`	Rounds an already computed value to a precision under a named mode.
`round_bounds(bounds, precision, mode)`	Rounds certified bounds to a single value at a precision.
`scalar_of(m)`	A magnitude of zero dimension as an exact `Rational`.
`sin_bounds(x, profile)`	Certified bounds of the sine of `x`.
`solve_linear(a, b)`	The root of `a·x + b = 0` over the rationals.
`sqrt_bounds(x, profile)`	Certified bounds of the square root of `x`.
`sum(xs)`	Exact sum of a collection of `Decimal`, `Money` or `Quantity` values.
`temp_convert(value, from, to, role, policy)`	Exact temperature conversion under an explicit versioned policy.
`text_length(t)`	Number of code points of a text after NFC normalization.
`unit_convert(m, unit)`	Converts a `Magnitude` to another unit of the same dimension.
`unit_exponent(m, unit)`	The exponent of a simple unit in the factors of a magnitude, as an exact `Integer`.
`weekday_of(d)`	Day of week of a date as an integer from 1 (Monday) to 7 (Sunday).
`with_unit(value, unit)`	Turns a dimensionless number into a `Quantity` of the named unit.
`year_end_of(d)`	December 31 of the calendar year containing the date.
`year_start_of(d)`	January 1 of the calendar year containing the date.

Run it

law engine check parking.law
law engine test tests/cheat-sheet.lawtest --program parking.law

Expected output:

check OK: parking.law

test PASS: the general rule
test PASS: unless withdraws the conclusion
test PASS: the refusal wins by priority
test PASS: no priority: the conflict is kept
test PASS: a defeater cancels support
test PASS: a definition
test PASS: an aggregate
test PASS: a value
test PASS: a deadline
test PASS: no policy, no deadline
test PASS: positions
test PASS: closure: on file without a record means not a resident
test PASS: closure: outside the domain silence stays silence
test PASS: an anchored rule applies while in force
test PASS: before it is in force the rule does not fire

Each section of this page has a scenario of its own; the one under Scenarios is the first of fifteen. To try a construct, change the facts of a scenario and run it again.

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

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