Argon by Example

Runnable, CI-verified example packages. Each is a real Argon package — build it with ox build examples/<name> and run it (ox run-scenario, ox query, ox derive, or ox test, per its README) — and its README.md explains what it teaches and shows the actual output. This index is generated from those READMEs and grouped by learning area.

36 example packages:

Getting started

Vocabulary & packages

Relations

Refinement & types

Rules, aggregates & recursion

Constraints & checks

Defeasible reasoning

Standpoints & federation

Bitemporal time

Modal operators

Traits

Testing

Capstone

Hello: the first program

Area: Getting started Teaches: the shape of an Argon source file — the std::core opt-in, a struct and an enum, a function, a derive rule, and the meta-calculus introducers (metaxis / metatype) that make the language vocabulary-neutral. Prerequisites: none — this is the entry point. Run: ox build examples/hello && ox check examples/hello

Argon ships zero built-in classifying vocabulary. Even type and rel — the keywords you declare a concept and a relation with — are not language keywords; they are the baseline introducers in std::core, brought in by an explicit use:

use std::core::{type, rel};

That single line is the whole story of the language’s neutrality: the words you classify your domain with are imported, never assumed. A foundational ontology like UFO is just another package you use — never something baked into the compiler.

What to read in root.ar

Ordinary data carriers — a struct and an enum. These are the value-level shapes, the parts of Argon that look like any modern typed language:

pub struct Diagnostic { severity: Severity, code: String, message: String }
pub enum Severity { Error, Warning, Info, Hint }

The meta-calculus introducers. A metaxis declares an axis of classification — a user-named dimension the compiler never reads the meaning of, only the lattice. A metatype is an introducer keyword built from positions on those axes:

pub metaxis rigidity for metatype { anti_rigid < semi_rigid < rigid };
pub metaxis sortality for metatype { sortal, non_sortal };

pub metatype kind = { rigidity: rigid, sortality: sortal };

After this, kind is usable as a declaration keyword for concepts — the same mechanism the vocabulary packages in this cluster (vocab_pkg_v0, metarel_vocab_v0) publish for other packages to import. hello declares the axes locally; the rest of the cluster shows them crossing a package boundary.

A function and a derive rule round out the file — the function is a pure value-level definition, the derive is a rule head over a body:

pub fn double(x: Int) -> Int = x * 2;
derive owes_tax(p) :- p.income > 0;

Running it

hello is the parser/elaboration smoke example — it declares forms but seeds no individuals, so there is nothing to query. Build it and check it:

$ ox build examples/hello
wrote examples/hello/target/root.oxbin (11 events, 6204 bytes)

$ ox check examples/hello --codes
ok

The artifact carries 11 events (one per declaration). ox check passes clean.

Honest caveats (what runs today)

• This package declares no pub query and no scenario, so ox query reports (module declares no \pub query` items). The owes_tax derive returns **0 tuples** (ox derive examples/hello owes_tax) — no Personindividuals are seeded andPersonhere has noincomefield, so the rule has nothing to fire on. The file is a *shape* demonstration, not a reasoning demonstration; for reasoning that produces rows, seeexamples/first_class_relationsandexamples/legal_norms_can_vote`.

This example is compiled and checked through the same ox pipeline the rest of the corpus uses; if a language change breaks its parse or elaboration, the build fails rather than the docs going stale.

Struct and enum values: data with no identity

Area: Getting started Teaches: the VALUE side of the value/ontology boundary — struct and enum as language built-ins (struct and enum). Pure data: structural equality, immutability, no metatype, no fact-store identity. How to construct a struct value, project a field, do a functional update with ..spread, build an enum payload value, read a payload back out with a value-position match, and read an optional field’s payload with the rule-body is Some(a) form. Prerequisites: hello (the shape of a source file). Run: ox check examples/struct_enum_values && ox test examples/struct_enum_values

Argon draws a line between ontology and data. A type (or any metatype-introduced concept) declares an entity with identity — an individual the fact store mints an id for, classifies, and reasons over. A struct or enum declares plain data: a value that is its contents, with no identity and no place in the metatype calculus. The two keywords are language built-ins, always available; the classifying vocabulary (type, rel) is imported.

This example is the data side. Everything here is a value.

A struct is its fields

pub struct Point { x: Int, y: Int }

pub fn origin() -> Point = Point { x: 0, y: 0 };
pub fn x_of(p: Point) -> Int = p.x;

A struct value is constructed by naming the type and giving every field. It is an ordinary expression — it can be a let binding, a field value, a function argument or return, a list element, or either side of a comparison. The postfix .x projects a field back out.

Equality is structural. Two struct values are equal when their fields are equal, field by field — there is no identity to tell them apart, and field order in the literal does not matter:

test "struct values are equal field-wise, order-independent" {
    assert Point { x: 1, y: 2 } == Point { y: 2, x: 1 };
    assert Point { x: 1, y: 2 } != Point { x: 1, y: 3 };
}

Immutability and ..spread

A struct value never changes. To get a value that differs in a few fields, copy an existing one and override those fields with the ..base spread — it yields a new value and leaves the base untouched:

test "spread overrides one field and leaves the base untouched" {
    let p = Point { x: 1, y: 2 };
    assert Point { ..p, x: 5 } == Point { x: 5, y: 2 };
    assert p == Point { x: 1, y: 2 };
}

Because the value is immutable, mut on a struct field is meaningless and refused (OE0253), and insert — which mints identity — is refused on a struct (OE0252). A struct is constructed as a value, never inserted.

Enum values, with and without a payload

pub enum Price { Cents(Int), Free }

A payloadless variant is a path: Price::Free. A payload variant carries one value and is built by applying the variant to it: Price::Cents(500). Enum values compare structurally too — same variant, same payload:

test "enum payload values compare structurally" {
    assert Price::Cents(500) == Price::Cents(500);
    assert Price::Cents(500) != Price::Cents(400);
    assert Price::Free != Price::Cents(0);
}

The struct-row table: a parameterized test

A struct value is the natural carrier for a parameterized test: one Case per scenario, looped with for. Each row is a value; the loop runs the same assertion over all of them.

pub struct Case { lhs: Int, rhs: Int, sum: Int }

test "addition over a table of struct cases" {
    for c in [
        Case { lhs: 0,  rhs: 0,  sum: 0 },
        Case { lhs: 2,  rhs: 3,  sum: 5 },
        Case { lhs: 20, rhs: 22, sum: 42 },
    ] {
        assert c.lhs + c.rhs == c.sum;
    }
}

Reading a payload back out

The idiomatic way to read or consume an enum value is a value-position match expression. Each arm names a variant; a payload arm binds the carried value into a fresh variable over the arm’s result. As an expression it sits anywhere a value can — a let right-hand side, a comparison operand, a fn body:

test "value-position match reads an enum payload" {
    let p = Price::Cents(500);
    assert (match p { Price::Cents(c) => c, Price::Free => 0 }) == 500;

    let free = Price::Free;
    assert (match free { Price::Cents(c) => c, Price::Free => 0 }) == 0;
}

For an optional field (age: Int?) inside a rule body, the reader is the membership test path is Some(binder): a present field binds the variable and contributes one row; an absent field contributes none, so the surrounding conjunction fails. is None is the absence test.

pub type Person { mut age: Int? }

pub derive Adult(p, a) :- p: Person, p.age is Some(a), a >= 18;
pub derive Ageless(p)  :- p: Person, p.age is None;

Running it

$ ox check examples/struct_enum_values --codes
ok

$ ox test examples/struct_enum_values
PASS  value-position match reads an enum payload
PASS  struct values are equal field-wise, order-independent
PASS  spread overrides one field and leaves the base untouched
PASS  projection reads a field off a struct value
PASS  enum payload values compare structurally
PASS  addition over a table of struct cases

6 passed, 0 failed, 0 errored, 0 inconclusive

Honest caveats (what runs today)

• A user-declared generic struct/enum (enum Opt<T> { … }) parses, but its type parameters reach no storage slot, so applying it (Opt<Int>) is refused (OE0235). The library generics Option<T> / Result<T, E> and the optional-field form T? are the supported parameterized shapes.
• A payload-binding match arm executes in value position (let r = match opt { Some(x) => x, None => 0 };, shown above) — but only there. The same arm in statement position (an effectful arm inside a mutate statement-match, e.g. match opt { Some(v) => { let _ = insert T { n: v }; }, None => {} }) is not yet executable — it is refused with OE1319 rather than mis-evaluated. Bind the payload in value position first, then run the effect. match over constant patterns (payloadless variants, literals, _) executes in both positions (pattern matching).
• A match over an enum declared in a different module (e.g. a test in tests/mod.ar matching an enum from root.ar) currently can’t resolve the scrutinee’s enum statically and is refused OE1319; keep the payload match in the same file as the enum (this example’s value-match test lives in root.ar).
• Calling a user fn inside a test assertion is not yet wired in the term evaluator, so the tests above construct and compare values directly rather than through the fn wrappers in root.ar. The functions still build and check; they are exercised by ox check / ox build.

This example is compiled, checked, and run through the same ox pipeline as the rest of the corpus; the whole-corpus gate (oxc-driver/tests/examples_corpus_gate.rs) ox checks it at source HEAD, so a language change that breaks its parse or elaboration fails CI rather than letting the docs go stale. The value-position payload-match semantics this example shows are independently gated end-to-end (construct, bind, select) by enum_payload_construct_equality_and_match_binding in oxc-driver/tests/cli_pipeline.rs.

Legal catalog — cross-package refusal fixture

Area: Vocabulary & packages Teaches: the negative companion to legal_catalog_v0 — pointing an imported directed_obligation’s creditor endpoint at a norm concept instead of a party is refused with OE0631 across the package boundary. Run: ox check examples/legal_catalog_bad_v0 --codes (must print OE0631 and exit non-zero)

Conformance fixture, not a tutorial. This package is designed to be refused. It exists so CI can prove a metarel-endpoint violation is caught across a package boundary — the constraint lives in the imported vocabulary, not in this file. For the well-formed consumer, read legal_catalog_v0; for the vocabulary, legal_vocab_v0.

The imported directed_obligation metarel constrains both endpoints to be party-sorted. This fixture points the creditor endpoint at PayRent, a norm concept (an obligation) — a directed obligation cannot run to a norm:

pub directed_obligation owesBad(debtor: Tenant, creditor: PayRent);

ox check must refuse this with OE0631 and exit non-zero — the endpoint check fires on the dependency-declared metarel:

$ ox check examples/legal_catalog_bad_v0 --codes
OE0631
$ echo $?
1

The full diagnostic names the offending position and both metatypes:

× OE0631: in `root::owesBad`, position 1 of relation `owesBad` is `PayRent`
│ (a `obligation`), but its classifying metarel `directed_obligation`
│ declares that position as `party` — an endpoint must be (a sub-metatype
│ of) the metarel's position metatype.

A corpus test (oxc-runtime/tests/examples_corpus.rs) asserts this package is refused with OE0631 — proving the metarel endpoint constraint survives the package join. If it regressed, this fixture would start building and CI would fail.

Consuming a vocabulary: imported checks run on your catalog

Area: Vocabulary & packages Teaches: the property that makes a vocabulary package real — when you import a vocabulary and declare concepts with its keywords, the vocabulary’s catalog checks run on your declarations at your own ox check/ox build. Cross-package static checking, for free. Prerequisites: the legal vocabulary package it imports. Run: ox build examples/legal_catalog_v0

legal_vocab_v0 ships deontic concepts, an introducer metatype obligation, and an OrphanObligationConcept check. This package imports the vocabulary, declares two norm concepts with its keyword, and the vocabulary’s check fires across the package boundary on this catalog — one well-formed, one orphan.

What to read in root.ar

Import the vocabulary’s keywords and concepts:

use legal_vocab_v0::{ obligation, party };
use legal_vocab_v0::{ LegalSubject, TimedObligation };

A well-formed norm anchors to the vocabulary’s root, so it inherits the deadline discipline and the check stays silent:

pub obligation PayRent <: TimedObligation { mut amount: Decimal }

An orphan norm anchors to nothing in the vocabulary — declared with the obligation keyword but specializing no norm root. This is exactly what OrphanObligationConcept is built to catch:

pub obligation Indemnify { mut scope: String }

Running it

ox build elaborates the two modules together and the vocabulary-shipped check fires on Indemnify (the orphan) while leaving PayRent (anchored) silent:

workspace: elaborated 2 module(s) into one artifact
UFOL::W002

  ⚠ UFOL::W002: an `obligation` concept does not specialize `TimedObligation`
  │ — anchor it so its deadline discipline is inherited [Indemnify]
  help: fired by check `legal_vocab_v0::OrphanObligationConcept`

The help: line names the check’s originating package — the diagnostic comes from the dependency, not from this file. The decisive contrast is PayRent vs Indemnify: both are declared with the imported obligation keyword, but only the orphan trips the imported audit. UFOL::W002 is a Warning, so the build succeeds (ox check --codes reports ok).

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the cross-package check behaviour, so the “imported checks run” property can’t drift from the language.

A legal deontic vocabulary package

Area: Vocabulary & packages Teaches: how to publish a vocabulary — a package whose pub surface is upper-ontology concepts, introducer metatypes, an endpoint-constrained metarel, and catalog checks that a consumer gets for free when it imports the package. Prerequisites: UFO constraints (metarel endpoints, meta, specializes), and the meta-calculus. Run: ox build examples/legal_vocab_v0 && ox check examples/legal_vocab_v0 --codes

Ontological vocabulary is never built into Argon and never in std — a modeler ships it as an ordinary package and a consumer depends on it by path. This is the deontic counterpart of vocab_pkg_v0: a UFO-L modeler ships the deontic concepts, the directed-obligation relation, and the audits a legal modeler inherits. Its consumer is legal_catalog_v0.

What to read in root.ar

An axis orders the modalities. deontic_force is pure user vocabulary — the compiler never reads a force name — ordering the three modalities by the strength of the constraint each imposes:

pub metaxis deontic_force for metatype { permission < obligation < prohibition };

Introducer metatypes become the consumer’s declaration keywords. A consumer writes pub obligation PayRent <: … and the introducer gate resolves the keyword across the dependency boundary. Each binds its force on the axis:

pub metatype permission  = { deontic_force::permission,  legal_kind::norm };
pub metatype obligation  = { deontic_force::obligation,  legal_kind::norm };
pub metatype prohibition = { deontic_force::prohibition, legal_kind::norm };

The deontic relation constrains both endpoints. A directed obligation runs from a debtor to a creditor — both party-sorted, never a contract or a bare individual. The endpoint metatypes are verified at elaboration; a relation declared with this introducer whose endpoint is not party-sorted is refused (see legal_catalog_bad_v0):

pub metarel directed_obligation(debtor: party, creditor: party);

The vocabulary ships its own checks. Every variable is TypeRef-sorted, so each #[static] check discharges at the consumer’s ox check, reading meta(k) / specializes. OrphanObligationConcept flags a norm-tagged concept that anchors to nothing in the vocabulary:

#[static]
pub check OrphanObligationConcept(k: TypeRef) :-
    meta(k) == obligation,
    not specializes(k, TimedObligation)
    => Diagnostic {
        severity: Severity::Warning,
        code:     "UFOL::W002",
        message:  "an `obligation` concept does not specialize `TimedObligation` — anchor it so its deadline discipline is inherited",
    };

Running it

The vocabulary itself checks clean — the checks fire on a consumer’s catalog, not on the vocabulary’s own declarations:

$ ox check examples/legal_vocab_v0 --codes
ok

The “free checks” property — that an imported check actually runs on the importing package — is demonstrated by the consumer legal_catalog_v0, where OrphanObligationConcept fires UFOL::W002 on the orphan norm concept.

This example is compiled in CI; the corpus auto-discovery parses and resolves it, and a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the package surface, so it can’t drift from the language.

metarel_consumer_bad_v0 — conformance fixture (must be refused)

Area: Vocabulary & packages Teaches: the negative companion to metarel_vocab_v0 — filling an imported metarel’s endpoint with the wrong metatype across a package boundary is refused with OE0631 at the consumer’s ox check. Run: ox check examples/metarel_consumer_bad_v0 --codes (must print OE0631 and exit non-zero)

This is a negative conformance fixture, not a tutorial. It depends on metarel_vocab_v0 and intentionally declares a relation with a wrong-sorted endpoint. It MUST fail ox check — that refusal is the whole point. For the teaching version, read metarel_vocab_v0.

What it does wrong

It imports the metatype-constrained characterization metarel from the separate metarel_vocab_v0 package — whose aspect_of position requires an aspect — and then fills that position with a kind:

use metarel_vocab_v0::{ kind, aspect, characterization };

pub kind Person;
pub kind Vehicle;

// WRONG: `aspect_of` requires an `aspect`, but `Vehicle` is a `kind`.
pub characterization inheresVia(bearer: Person, aspect_of: Vehicle);

The constraint lives in the dependency, not in this file — so this fixture proves the endpoint-metatype check survives the package join and is enforced at the consumer’s ox check.

Required behavior

ox check must refuse it with OE0631 and exit non-zero:

$ ox check examples/metarel_consumer_bad_v0 --codes
OE0631
$ echo $?
1

Full diagnostic:

Error: OE0631
  × OE0631: in `root::inheresVia`, position 1 of relation `inheresVia` is
  │ `Vehicle` (a `kind`), but its classifying metarel `characterization`
  │ declares that position as `aspect` — an endpoint must be (a sub-metatype
  │ of) the metarel's position metatype.

This package must never build clean. The pipeline test (oxc-driver/tests/cli_pipeline.rs) asserts the OE0631 refusal through the real ox binary; if a change lets it pass, the test fails.

A metarel with metatype-constrained endpoints

Area: Vocabulary & packages Teaches: an introducer metarel can constrain the metatype of each endpoint position, and that constraint travels with the published metarel — a consumer’s relation endpoints are verified against it across the package boundary. Prerequisites: publishing a vocabulary (introducer metatypes and metarels). Run: ox build examples/metarel_vocab_v0 && ox check examples/metarel_vocab_v0

A relation is not just a tuple of types — in a vocabulary it often carries an ontological constraint on what kind of thing may sit in each slot. UFO’s characterization relates a bearer to an aspect: the bearer must be a substantial kind, the second slot must be an aspect. metarel_vocab_v0 publishes exactly that shape, so a separate consumer that fills a slot with the wrong sort of thing is refused at its own ox check. (The refusal itself is the companion fixture, metarel_consumer_bad_v0.)

What to read in root.ar

An axis, then two introducer metatypes positioned on it. The axis names are pure user vocabulary — the compiler reads the lattice, never the meaning of the words:

pub metaxis sortality for metatype { sortal, non_sortal };

pub metatype kind   = { sortality::sortal };
pub metatype aspect = { sortality::non_sortal };

A metarel whose endpoints are metatype-constrained. Position 0 (bearer) must be kind-sorted; position 1 (aspect_of) must be aspect-sorted. These position metatypes are part of the published metarel:

pub metarel characterization(bearer: kind, aspect_of: aspect);

When a consumer in another package declares a characterization relation, the endpoint metatypes of its relation are checked against these positions. An endpoint must be (a sub-metatype of) the position’s metatype, or ox check refuses it across the dependency boundary — the same refusal an in-package violation gets.

Running it

The vocabulary checks clean — it only publishes the constrained metarel, it doesn’t use it:

$ ox build examples/metarel_vocab_v0
wrote examples/metarel_vocab_v0/target/root.oxbin (4 events, 2393 bytes)

$ ox check examples/metarel_vocab_v0 --codes
ok

To see the constraint bite, point a consumer at this package and have it fill aspect_of with a kind — that is examples/metarel_consumer_bad_v0, which is refused OE0631.

Honest caveats (what runs today)

• This package declares no individuals and no pub query; it is pure vocabulary. The endpoint constraint is enforced statically, at a consumer’s ox check, not at runtime.

This vocabulary and its (deliberately failing) consumer are driven through the real ox binary by a pipeline test (oxc-driver/tests/cli_pipeline.rs): the test pins that this package checks clean and that a wrong-sorted endpoint in the consumer is refused OE0631, so the cross-package endpoint check can’t drift from the language.

Consuming a vocabulary across a package boundary

Area: Vocabulary & packages Teaches: a modeler package depends on a separate vocabulary package, imports its introducer metatypes/metarel, and uses them as its own declaration keywords — and the vocabulary’s catalog check fires on this package’s catalog at ox check. Prerequisites: the vocabulary author side — read that first. Run: ox build examples/vocab_consumer_v0 && ox check examples/vocab_consumer_v0

This is the consumer side. vocab_consumer_v0 owns no vocabulary of its own; it declares a path dependency on vocab_pkg_v0 and models its domain entirely with imported keywords. This is the property that makes vocabulary packages real: the modeler classifies with words it doesn’t own, and the introducer gate resolves them across the dependency boundary.

What to read

ox.toml declares the dependency. The key is the path root the consumer imports under, and it must equal the dependency’s package name:

[dependencies]
vocab_pkg_v0 = { path = "../vocab_pkg_v0" }

root.ar imports the vocabulary and declares with it. The introducer metatypes (category, kind) and the metarel (characterization) come from the dependency — this package never declares them:

use vocab_pkg_v0::{ category, kind, characterization };
use vocab_pkg_v0::{ Endurant, Substantial, Detached };

pub kind Person <: Substantial { name: String }
pub category Dwelling <: Endurant;
pub characterization Inhabits(p: Person, d: Dwelling);

Person is declared with the dependency’s kind keyword and specializes the dependency’s Substantial — well-formed.

One declaration deliberately trips the vocabulary’s check. Ghost is a kind that specializes Detached, which is exactly what vocab_pkg_v0’s shipped OrphanKind check warns about:

pub kind Ghost <: Detached;

Running it

ox check resolves the dependency, declares Ghost with the imported kind, and the imported OrphanKind check fires on it — a non-fatal warning that names the offending type and the check that fired:

$ ox check examples/vocab_consumer_v0
UFO::W001

  ⚠ UFO::W001: a `kind` specializes `Detached` — specialize `Substantial`
  │ instead [Ghost]
  help: fired by check `vocab_pkg_v0::OrphanKind`

ok

The decisive detail is fired by check \vocab_pkg_v0::OrphanKind`: the check the modeler is being held to was authored in a package it merely depends on. The build still completes — UFO::W001is aWarning`, not an error:

$ ox build examples/vocab_consumer_v0
workspace: elaborated 2 module(s) into one artifact
UFO::W001
  ⚠ UFO::W001: a `kind` specializes `Detached` — specialize `Substantial` instead [Ghost]
  help: fired by check `vocab_pkg_v0::OrphanKind`
wrote examples/vocab_consumer_v0/target/root.oxbin (13 events, 7182 bytes)

Honest caveats (what runs today)

• UFO::W001 is a Warning, so ox check --codes prints ok (no error codes) even though the warning is emitted. Read the full ox check output (not --codes) to see the warning text.

This consumer and its vocabulary are driven through the real ox binary by a pipeline test (oxc-driver/tests/cli_pipeline.rs): the test pins that this package elaborates against the dependency and that the vocabulary-shipped OrphanKind check fires on Ghost, so the cross-package check can’t drift from the language.

Vocabulary package: publishing your own classifying vocabulary

Area: Vocabulary & packages Teaches: a package can publish its own introducer metatypes, an introducer metarel, upper categories, and a catalog check — the building blocks a foundational ontology like UFO is made of. None of this is built into the language; it is all ordinary pub surface. Prerequisites: the meta-calculus introducers (metatype / metarel), see hello. Run: ox build examples/vocab_pkg_v0 && ox check examples/vocab_pkg_v0

This is the author side of the two-package vocabulary journey. vocab_pkg_v0 ships a small UFO-shaped vocabulary; vocab_consumer_v0 (a separate package) depends on it. The point is that Argon has no privileged ontology: a vocabulary is a normal package, and everything that makes UFO “UFO” — the kinds, the categories, the well-formedness checks — lives on this package’s public surface.

What to read in root.ar

Introducer metatypes — declaration keywords for the consumer. A metatype published pub becomes a keyword a downstream package declares its concepts with:

pub metatype category = { };
pub metatype kind = { };

A binary introducer metarel. Same idea, for relations: a published metarel is a keyword for declaring relations downstream:

pub metarel characterization<A, B>(a: A, b: B);

Upper-ontology categories the consumer specializes. These are concepts declared with the package’s own category introducer, forming a small hierarchy the consumer hangs its domain off of:

pub category Endurant;
pub category Substantial <: Endurant;
pub category Detached    <: Endurant;

A catalog check the vocabulary ships — and that fires on the consumer’s catalog. This is what makes a vocabulary package real rather than decorative. The check is #[static] and every variable is TypeRef-sorted, so it discharges at ox check/ox build time over the catalog of declared types — not over runtime individuals:

#[static]
pub check OrphanKind(k: TypeRef) :-
    meta(k) == kind,
    specializes(k, Detached)
    => Diagnostic {
        severity: Severity::Warning,
        code:     "UFO::W001",
        message:  "a `kind` specializes `Detached` — specialize `Substantial` instead",
    };

It reads the reflective intrinsics meta (the metatype a concept was introduced with) and specializes (the declared hierarchy). It flags any kind that specializes Detached. Crucially, the check is written here, in the vocabulary, but it runs against the consumer’s pub kind declarations — imported checks travel with the vocabulary.

Running it

The vocabulary checks clean on its own — it declares no offending kind itself:

$ ox build examples/vocab_pkg_v0
wrote examples/vocab_pkg_v0/target/root.oxbin (7 events, 4334 bytes)

$ ox check examples/vocab_pkg_v0 --codes
ok

To see OrphanKind actually fire, you need a consumer with a catalog that violates it — that is the next example, vocab_consumer_v0.

Honest caveats (what runs today)

• This package declares no pub query and no individuals; it is pure vocabulary. Its value is realized at a consumer’s ox check — vocab_pkg_v0 alone has nothing for the check to fire on.

This example and its consumer are driven through the real ox binary by a pipeline test (oxc-driver/tests/cli_pipeline.rs): the test pins that this package checks clean and that OrphanKind fires on the consumer’s catalog, so the cross-package check can’t drift from the language.

First-class relations

Area: Relations Teaches: relations are first-class constructs — n-ary, with their own properties, cardinality, specialization, and rule participation. Prerequisites: concepts and <: (see concepts and hierarchies). Run: ox build examples/first_class_relations && ox query examples/first_class_relations

In most data languages a relationship is a second-class thing: a foreign key with no identity and no data of its own, or something you reify by hand into a stand-in node. Argon makes a relation a construct, declared with a rel keyword exactly as a concept is declared with a type keyword. An edge has the same standing as a node.

What to read in root.ar

A relation carries its own data. An employment has a salary — the salary belongs to the relationship, not to the person or the org:

pub rel Employment(employee: Person, employer: Org) { mut salary: Int };

Cardinality is per endpoint (UML association-end multiplicity — the i-th bracket bounds the distinct position-i values for a fixed combination of the other endpoints): [0..1] on the owner slot means an asset has at most one owner, and [0..*] on the asset slot means a person may own any number.

pub rel Owns(owner: Person, asset: Asset) [0..1] [0..*];

Relations are n-ary, not just binary — a sale relates three participants without an intermediate node:

pub rel Sale(seller: Person, buyer: Person, item: Asset);

Relations specialize, like concepts — every internship is an employment:

pub rel Internship(employee: Person, employer: Org) <: Employment;

Relations participate in rules, read in a rule body exactly as a concept’s extent is:

pub derive colleagues(a: Person, b: Person) :- Employment(a, o), Employment(b, o);

Running it

With Alice and Bob both employed by Acme, colleague_pairs returns the four pairings the rule derives — including each person with themselves, since the rule as written does not exclude a = b (adding an inequality guard is a natural exercise).

Honest caveats (what runs today)

• Maximum cardinality is enforced at the write path; a minimum above zero (e.g. [1..1]) is recorded on the wire but not yet enforced in v0 — ox check emits OW1342 naming the relation and position. This example uses [0..1] / [0..*], so it has no unenforced minimum.

This example is compiled and run in CI — the corpus auto-discovery parses and resolves it, and a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the colleague_pairs behaviour to exactly the four pairings the rule derives. If the language changes underneath it, the build breaks rather than the docs going stale.

UFO constraints — refusal fixture

Area: Relations Teaches: the negative companion to ufo_constraints_v0 — a metarel endpoint filled with the wrong metatype is refused with OE0631 at ox check, pinning the endpoint-constraint diagnostic. Run: ox check examples/ufo_constraints_bad --codes (must print OE0631 and exit non-zero)

Conformance fixture, not a tutorial. This package is designed to be refused. It exists so CI can prove ox check rejects a metarel-endpoint violation, and so the diagnostic stays pinned. For the feature it guards, read ufo_constraints_v0.

The characterization metarel requires its aspect position (position 1) to be aspect-sorted. This fixture fills that position with Vehicle, a kind — an ability would have to inhere via a vehicle, not via an aspect:

pub characterization inheresVia(bearer: Person, aspect_of: Vehicle);

ox check must refuse this with OE0631 and exit non-zero:

$ ox check examples/ufo_constraints_bad --codes
OE0631
$ echo $?
1

The full diagnostic names the offending position and both metatypes:

× OE0631: in `<anonymous>::inheresVia`, position 1 of relation `inheresVia`
│ is `Vehicle` (a `kind`), but its classifying metarel `characterization`
│ declares that position as `aspect` — an endpoint must be (a sub-metatype
│ of) the metarel's position metatype.

A corpus test (oxc-runtime/tests/examples_corpus.rs) asserts this package is refused with OE0631 — if the endpoint check regressed and this fixture started building, CI would fail.

UFO constraints: metarel endpoints, signature reflection, per-type axis override

Area: Relations Teaches: the three relation/meta-property features a UFO vocabulary author needs — a metarel that constrains its endpoints’ metatypes, a derive/check that reflects over relation signatures (rel/arm/meta) to audit them, and a per-type axis override that wins over the metatype default. Prerequisites: first-class relations, and the meta-calculus (metaxis / metatype / metarel, meta). Run: ox build examples/ufo_constraints_v0 && ox derive examples/ufo_constraints_v0/target/root.oxbin aspectEndpointIsAspect

A vocabulary author building an upper ontology (UFO) does not just declare concepts — they declare the rules of well-formedness for the modelers who consume the vocabulary, and they want the compiler to enforce them. This example is the well-formed proof of three such features; its sibling ufo_constraints_bad is the refusal half.

What to read in root.ar

A metarel constrains its endpoints’ metatypes. characterization is a binary introducer metarel; its bearer position must be kind-sorted and its aspect position must be aspect-sorted. An ability inheres via an aspect, not a kind — and the compiler verifies it at elaboration:

pub metarel characterization(bearer: kind, aspect_of: aspect) {
    dependency_kind::existential,
};

A relation declared with this introducer whose endpoints match is well-formed; inheresVia does, because Person is a kind and Ability is an aspect:

pub characterization inheresVia(bearer: Person, aspect_of: Ability) [1..1] [0..*];

A vocabulary audits relation signatures declaratively. rel(r, characterization) enumerates every relation classified by the metarel; arm(r, 1, t) reads its position-1 endpoint type; meta(t) reads that type’s metatype. Joined together, the vocabulary checks its own endpoint discipline — r and t are TypeRef-sorted, so this derives at the catalog tier:

pub derive aspectEndpointIsAspect(r: TypeRef, t: TypeRef) :-
    rel(r, characterization), arm(r, 1, t), meta(t) == aspect;

pub derive aspectEndpointIsKind(r: TypeRef, t: TypeRef) :-
    rel(r, characterization), arm(r, 1, t), meta(t) == kind;

A type can override an axis its metatype binds. Role is introduced by kind, whose metatype binds rigidity::rigid — but a role is anti-rigid. The per-target override sets the type’s own effective rigidity, and the type-keyed t.rigidity projection reads the override, not the metatype default:

pub kind Role { rigidity::anti_rigid }

pub derive antiRigidTypes(t: TypeRef) :- t.rigidity == rigidity::anti_rigid;

Running it

The vocabulary’s own audit confirms the discipline holds. The aspect endpoint of every characterization relation is aspect-sorted (so the well-formed set is the whole set), and no characterization relation has a kind in its aspect slot:

derive(aspectEndpointIsAspect): 1 tuple(s)
  (<anonymous>::inheresVia, <anonymous>::Ability)
derive(aspectEndpointIsKind): 0 tuple(s)

The override wins: antiRigidTypes returns three types — aspect and Ability (anti-rigid by their metatype) and Role, whose per-target override beats the rigid it inherits from kind:

derive(antiRigidTypes): 3 tuple(s)
  (<anonymous>::aspect)
  (<anonymous>::Ability)
  (<anonymous>::Role)

Honest caveats (what runs today)

• Maximum cardinality is enforced at the write path; a minimum above zero is recorded on the wire but not yet enforced in v0. inheresVia declares [1..1] at its bearer position, so ox build emits OW1342 naming the relation and position — a warning, not a refusal; the build succeeds.

This example is compiled and run in CI — the corpus auto-discovery parses and resolves it, and a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the reflection and override behaviour. If the language changes underneath it, the build breaks rather than the docs going stale.

Refinement with multi-field predicates

Area: Refinement & types Teaches: a refinement predicate is an ordinary boolean expression — it can read several fields and combine them with &&/||, comparisons, and string equality. Prerequisites: refinement (iff/where). Run: ox build examples/multi_field_refinement && ox run-scenario examples/multi_field_refinement

A single iff refinement classifies a Person by two fields at once:

pub type ActiveAdult <: Person iff {
    self.age >= 18 && self.status == "active"
};

ActiveAdult is the subset of people who are both adults and active. The predicate is evaluated per individual at query time against that individual’s declared fields — no membership is stored.

Running it

The scenario registers four people; only those satisfying both conjuncts are classified:

alice  age=25  status="active"    → ActiveAdult
bob    age=12  status="active"    → not (fails age >= 18)
carol  age=30  status="inactive"  → not (fails status == "active")
dave   age=45  status="active"    → ActiveAdult

so active_adults returns 2 rows (alice, dave) out of the 4 in all_people.

This example is compiled and run in CI; its runtime behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs).

Refinement: iff (defined) vs where (primitive)

Area: Refinement & types Teaches: the two ways a refined concept gets its members — iff derives membership from a predicate, where asserts membership and treats the predicate as an enforced invariant. This is the most consequential distinction in Argon’s type layer. Prerequisites: concepts and <: specialization. Run: ox build examples/primitive_refinement && ox run-scenario examples/primitive_refinement

Two refined concepts sit over one Person population, and the keyword decides who is a member:

// Defined: anyone satisfying the predicate is automatically a member.
pub type Adult   <: Person iff   { self.age >= 18 };

// Primitive: membership is granted by an authority; the predicate is a
// necessary invariant on members, checked at the grant — never a classifier.
pub type Cleared <: Person where { self.clearance_score >= 50 };

• iff (Adult) — membership is derived. You never assert it; the reasoner classifies every Person whose age >= 18. Asserting it directly (insert iof(p, Adult)) is refused with OE0211.
• where (Cleared) — membership is asserted. A clearance is conferred by an act (grant_clearance → insert iof(p, Cleared)); the predicate only guards that act. A qualifying score is necessary, not sufficient.

The teaching contrast

Run it and compare the two extents. After the scenario seeds four people:

query clearance::adults:  4 row(s)   — Adult (iff):   everyone 18+, auto-classified
query clearance::cleared: 2 row(s)   — Cleared (where): only the two who were granted

The decisive case is dave: he has clearance_score = 70 (≥ 50) but was never granted, so he is not Cleared. Under iff he’d be classified automatically; under where membership is conferred, never inferred.

Honest caveats (what runs today)

• Granting clearance below the invariant is rejected with OE0668 (the where predicate is enforced at the grant). Inserting an iff membership directly is refused with OE0211.
• Refinement membership is evaluated by the reasoner at query time against each individual’s fields, so the extents above reflect the seeded age/score values.

This example is compiled and run in CI; its iff/where runtime behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so it can’t drift from the language.

A small employment ontology: refinement + a concept hierarchy

Area: Refinement & types Teaches: how iff refinements layer over a concept hierarchy (<:), with mutable fields populated by a mutate and read back through queries — a realistic, end-to-end shape. Prerequisites: refinement (iff/where). Run: ox build examples/refinement_employment && ox run-scenario examples/refinement_employment

pub type Person   { mut weekly_hours: Int, mut direct_reports: Int }
pub type Employee <: Person;
pub type FullTime <: Employee iff { self.weekly_hours  >= 35 };
pub type Manager  <: Employee iff { self.direct_reports >= 1 };

Employee specializes Person; FullTime and Manager are defined subsets of Employee — a person is classified into them automatically by their fields, and is reclassified when those fields change. A single hire mutation establishes a person and populates the fields:

pub mutate hire(p: Person, hours: Int, reports: Int) {
    insert iof(p, Person);
    insert iof(p, Employee);
    update p: Person set { weekly_hours = hours, direct_reports = reports }
}

Running it

The scenario hires several people; full_timers and managers come back as the filtered subsets of the all_persons extent — the iff predicates evaluated per individual at query time. Change someone’s weekly_hours below 35 and they leave FullTime on the next read; classification follows the data.

This example is compiled and run in CI; its refinement behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs).

Aggregates: count and exists in rule bodies

Area: Rules, aggregates & recursion Teaches: the aggregate forms exists { B } and count { B } cmp N inside a derive body — a subquery whose cardinality (or mere non-emptiness) drives the head. Aggregation is part of the rule language, not a separate report step. Prerequisites: concepts and <: specialization, and derive rule bodies (see first-class relations). Run: ox build examples/aggregate_count_v0 && ox derive examples/aggregate_count_v0 <predicate>

A data language that cannot count inside a rule pushes every cardinality question out to application code. Argon admits an aggregate atom as a subquery in the body: exists { B } is true when B has any solution, and count { B } yields the number of solutions so a comparison atom can filter on it.

What to read in company.ar

The corpus is three people, one of them a manager:

pub fact Person(alice);
pub fact Person(bob);
pub fact Person(carol);
pub fact Manager(alice);

exists { B } is a bare Boolean — the head fires iff the body has at least one solution:

pub derive any_person()  :- exists { Person(p) };
pub derive any_manager() :- exists { Manager(p) };

count { B } cmp N compares the cardinality. The aggregate binds the count to a synthesized variable; the comparison atom is the filter:

pub derive at_least_three_persons() :- count { Person(p) } >= 3;
pub derive thin_management()        :- count { Manager(p) } < 2;
pub derive huge_company()           :- count { Person(p) } >= 100;

These heads are 0-ary: each is a propositional flag that either fires or does not.

Running it

ox derive <predicate> prints the derived tuples. A 0-ary head that fires returns exactly one tuple — the empty tuple (); one that does not fire returns none:

derive(any_person):              1 tuple(s)   ()   — three Persons exist
derive(any_manager):             1 tuple(s)   ()   — alice is a Manager
derive(at_least_three_persons):  1 tuple(s)   ()   — count{Person} = 3, so >= 3 holds
derive(thin_management):         1 tuple(s)   ()   — count{Manager} = 1, so < 2 holds
derive(huge_company):            0 tuple(s)        — count{Person} = 3, so >= 100 fails

The decisive contrast is at_least_three_persons vs huge_company: the same count { Person(p) } subquery (which evaluates to 3) yields opposite verdicts because the threshold differs. The count is computed inside the rule, not handed to the rule.

Honest caveats (what runs today)

• v0 admits count (and bare exists) with the comparison operators ==, !=, <, <=, >, >=. The comprehension form (sum(expr for x in S where φ)), aggregators beyond count / count_distinct, and nested aggregates are γ follow-ons of RFD 0011.
• A 0-ary head models a proposition: one tuple means true, zero tuples means false. The single tuple is the empty tuple ().
• This package builds and runs under ox; unlike its sibling aggregate_membership_join it is not yet pinned by a corpus test, so it documents the surface rather than a regression.

Aggregates: counting inside a join

Area: Rules, aggregates & recursion Teaches: a count { B } whose body B is a join — a relation atom together with a type-membership atom (p in Person) — so the count ranges only over partners that satisfy both. The membership filter and the relation join are the same body; reordering them must not change the count. Prerequisites: aggregates (count / exists), and first-class relations. Run: ox build examples/aggregate_membership_join && ox derive examples/aggregate_membership_join <predicate>

count { Person(p) } counts a population; count { R(a, p) } counts edges. The interesting case is the conjunction — count the R-partners of a that are also Persons — because the membership atom and the relation atom must be solved together, and a bug that drops the membership test silently under-joins to zero.

What to read in root.ar

a0 relates via R to three things, but only two of them (p1, p2) are Persons — p3 is a plain Thing:

pub fact R(a0, p1);   // p1 in Person
pub fact R(a0, p2);   // p2 in Person
pub fact R(a0, p3);   // p3 in Thing, NOT Person

Relation-only count ranges over all three R-partners:

pub derive rel_count_is_three(a) :- Thing(a), count { R(a, p) } >= 3;

Count inside a join intersects the relation with type membership, so only the Person-typed partners count — two, not three:

pub derive member_count_at_least_two(a)   :- Thing(a), count { p in Person, R(a, p) } >= 2;
pub derive member_count_at_least_three(a) :- Thing(a), count { p in Person, R(a, p) } >= 3;

Order-independence — swapping the two body atoms is the same join, so the same count of 2:

pub derive member_count_reordered_two(a) :- Thing(a), count { R(a, p), p in Person } >= 2;

Running it

ox derive <predicate> prints the head’s tuples; each firing head returns the bound a (here the individual a0):

derive(rel_count_is_three):           1 tuple(s)   (a0)   — count{R(a,p)} = 3, so >= 3 holds
derive(member_count_at_least_two):    1 tuple(s)   (a0)   — count{p in Person, R(a,p)} = 2, so >= 2 holds
derive(member_count_at_least_three):  0 tuple(s)          — that count is 2, so >= 3 fails
derive(member_count_reordered_two):   1 tuple(s)   (a0)   — reordered body, same count of 2

The decisive contrast is rel_count_is_three vs member_count_at_least_three: both ask >= 3 of a count over a0’s R-partners, but the membership atom drops p3 (a non-Person), so the count falls from 3 to 2 and the second head does not fire. The member_count_reordered_two head proves the count is independent of atom order — both arrangements solve the same join.

Honest caveats (what runs today)

• The join inside the aggregate is the ordinary conjunctive body: p in Person is a type-membership atom and R(a, p) is a relation atom, solved together over the shared variable p.
• The count ranges over distinct solution bindings of the body, evaluated against the current state.

This example is compiled and run in CI; its join-count behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs::corpus_aggregate_membership_join_count), so the membership-inside-aggregate semantics can’t regress to the silent under-count it was written to guard against.

Double-entry accounting: aggregates, balance, and an invariant

Area: Rules, aggregates & recursion Teaches: quantitative modeling that was inexpressible declaratively before RFD 0029 — a rule head that carries a computed value, two aggregates compared (the double-entry invariant as a single check), exact Decimal money end to end, and banker’s rounding. Plus in-language test blocks that assert against the derived plane. Prerequisites: first-class relations (the postings join through relations); check constraints. Run: ox build examples/double_entry_v0 && ox run-scenario examples/double_entry_v0 — and ox test examples/double_entry_v0

Double-entry is the canonical small accounting model: every transaction posts a debit and a matching credit, and the books balance when, within every journal entry, total debits equal total credits. It is also the exact wall RFD 0029 broke through — a rule head could not carry a computed value, and two aggregates could not be compared, so neither a per-account balance nor the balancing invariant could be written.

What to read in ledger.ar

A head carries a computed value. The per-account balance is Σ debits − Σ credits, grouped by the outer-bound acct; both aggregates bind to a variable, then bal is a derived value:

pub derive accountBalance(acct, bal) :- acct: Account,
    debits  = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    credits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "C"),
    bal     = debits - credits;

The invariant compares two aggregates — a balanced entry derives nothing, an unbalanced one fires the check:

pub check EntryNotBalanced(e: Entry) :-
    e: Entry,
    debits  = sum(p.amount for p in Posting, inEntry(p, e), p.side == "D"),
    credits = sum(p.amount for p in Posting, inEntry(p, e), p.side == "C"),
    debits != credits
    => Diagnostic { severity: Severity::Error, code: "Ledger::E001", /* … */ };

Money is exact, with banker’s rounding. A Decimal stays a Decimal — never via f64 — and round_half_even ties to even (the money default, avoiding the upward bias of half-away-from-zero):

pub derive accountTax(acct, tax) :- acct: Account,
    debits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    raw    = debits * 0.075,
    tax    = round_half_even(raw, 2);

Running it

ox run-scenario posts two balanced entries (Cash 100.50 / Revenue 100.50 and Cash 50.25 / Revenue 50.25), each leg pair committing atomically so the EntryNotBalanced Error guard is satisfied at every committed state:

scenario: applied 6 mutation(s) from examples/double_entry_v0/demo.toml

The interesting outputs are the derived values themselves, and the package asserts them directly with in-language test blocks. ox test runs each test "name" { … } against a fresh store and reports pass/fail:

PASS  a constructed account carries its name
PASS  postings carry exact decimal amounts and sides
PASS  an entry carries its memo and a second posting still reads back
PASS  accountBalance derives the posted amount per account
PASS  accountDebits derives the debit total per account
PASS  a balanced entry is derivable
PASS  an unbalanced entry is not derivable as balanced
PASS  an auto-discovered tests/ file runs its tests

8 passed, 0 failed, 0 errored, 0 inconclusive

The accountBalance test asserts accountBalance(cash) == 100.50 against the reasoner’s materialized extent — a deductive-plane assert, the point of testing a reasoning system. After the full demo harness the books read: accountBalance = {(cash, 150.75), (revenue, -150.75)}, and accountTax(cash) = round_half_even(11.30625, 2) = 11.31 (rounded to cents under round-half-even — here .30625 is past the half-cent, so it rounds up; the tie-to-even rule only changes the result on an exact x.xx5 boundary).

Honest caveats (what runs today)

• The ledger’s interesting predicates are pub derive, not pub query, so ox run-scenario --extent <name> (a concept extent lookup) does not enumerate them — the derived values are read through ox test asserts and the corpus pin instead.
• assert [not] derivable F(args) reads with world-honest three-valued semantics keyed on F’s world assumption. These concepts are closed-world (the package default), so absence is definite non-derivability — both derivable and not derivable are assertable here.
• The second tests/derived.ar file is auto-discovered by ox test but is not mod-wired into root.ar, so ox build never sees it (test-mode only).

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the exact decimal balances (150.75 / −150.75), the per-account totals, and the banker’s-rounded tax (11.31), so the aggregate semantics can’t drift from the language.

Robot plan execution: three reasoning regimes on one model

Area: Rules, aggregates & recursion Teaches: a planning/robotics domain over a self-defined upper ontology, exercising three workhorse reasoning regimes on one package — a true bounded forall, a mutually-recursive least fixpoint, and arbitration by recursion through negation under well-founded semantics. Also: an upper ontology is an ordinary module, not a language built-in. Prerequisites: first-class relations; derive rule bodies; negation-as-failure. Run: ox build examples/robot_plan_execution && ox query examples/robot_plan_execution

A mobile robot executes a plan: charge, navigate, scan, pick up. Two modules split the model deliberately — upper is a minimal upper ontology defined in this package (Object, Event, Capability, a derived involves), and robot specializes it (Agent <: Object, Action <: Event, Skill <: Capability) and builds the planner. Argon is ontology-neutral: a published foundational ontology could be imported in upper’s place without touching the domain.

What to read in robot.ar

A true universal — the bounded forall. An action is ready-at-start when every one of its preconditions holds initially. This lowers to a count-equality, not the existential “some precondition holds” (an action with no preconditions is vacuously ready):

pub derive readyAtStart(a: Action) :-
    Action(a),
    forall f: Fluent where pre(a, f), holds(f);

A mutually-recursive least fixpoint — forward reachability. A fluent is reachable if it holds initially or is added by an applicable action; an action is applicable when none of its preconditions is unreachable. The universal “all preconditions reachable” is the standard double-negation encoding, because a forall may not sit inside a recursive cycle on this engine — the alternating fixpoint converges it:

pub derive unreached(a: Action) :- pre(a, f), not reachable(f);
pub derive applicable(a: Action) :- Action(a), not unreached(a);
pub derive reachable(f: Fluent) :- adds(a, f), applicable(a);

Arbitration — recursion through negation. Two conflicting actions cannot both run. scheduled recurses through its own negation via challenged, so {scheduled, challenged} form one NAF-cyclic SCC the engine evaluates by well-founded semantics directly (strict stratification would reject this):

pub derive challenged(a: Action) :- conflicts(a, b), scheduled(b);
pub derive scheduled(a: Action)  :- applicable(a), not challenged(a);

Running it

ox query enumerates every declared pub query. The plan chain closes over all seven fluents and all seven actions are applicable; the arbitration is the payoff:

query robot::reachableFluents:   7 row(s)
query robot::applicableActions:  7 row(s)
query robot::readyActions:       1 row(s)    — only `charge` (pre {atHome}, true at start)
query robot::scheduledActions:   4 row(s)    — {charge, navigate, scan, pickup}
query robot::challengedActions:  1 row(s)    — {pushObject}
query upper::involvement:        1 row(s)    — (pickup, rob): pickup exercises a capability rob bears

Two conflicts drive the arbitration. The asymmetric one resolves to a definite winner: pushObject is challenged by the higher-priority pickup, pickup has no rival so it is never challenged, so pickup is scheduled and pushObject is not. The symmetric one (wipeLeft ↔ wipeRight, no tiebreak) is well-founded-undefined: the engine materializes only definitely-true atoms, so neither appears in scheduled and neither appears in challenged — that absence-of-both is the deadlock’s observable signature.

Honest caveats (what runs today)

• ox query renders rows as opaque individual ids; the row counts and the named membership above are what the corpus test pins (it resolves the ids back to names).
• Arbitration is kept as a single SCC on purpose. Splitting it into a lower blocked stratum and a higher scheduled :- not blocked would ask the engine to read a well-founded relation under a higher negation — it materializes the WFS stratum two-valued at that boundary, so a genuinely-undefined atom would read as false downstream and over-assert. The single-SCC form is the sound one.

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins scheduled = {charge, navigate, scan, pickup}, challenged = {pushObject}, and the absence of both symmetric-deadlock actions, so the well-founded arbitration can’t drift from the language.

Check constraints: diagnostics on two moments

Area: Constraints & checks Teaches: check rules — constraint/integrity rules that emit a Diagnostic instead of populating an IDB. Where a check discharges is decided by its vocabulary: a catalog-level (TypeRef-sorted) check fires at build, an instance-level check is a runtime delta guard, and one whose EDB is partly declared in source fires at both moments. Prerequisites: concepts and <: specialization; refinement (iff/where) helps. Run: ox build examples/check_constraints && ox run-scenario examples/check_constraints

A check is not a derive. It has no head extent; it computes a condition and, when the condition holds, raises a coded Diagnostic. Argon is a constraint language, and a check is the unit of constraint. The decisive idea here is that the sort of a check’s variables tells the compiler when it can be discharged.

What to read in fleet.ar

A catalog-level check discharges at build. Every variable is TypeRef-sorted, so the condition is decidable over the declared types alone — no instances needed. #[static] makes that a contract: if the body ever drifts to instance vocabulary, the build fails with OE1322 rather than silently reclassifying to a runtime guard.

#[static]
pub check NoDeprecatedVehicles(t: TypeRef) :-
    specializes(t, Deprecated),
    t != Deprecated
    => Diagnostic {
        severity: Severity::Warning,
        code:     "Fleet::W001",
        message:  "type still specializes Deprecated — migrate it before v2",
    };

An instance-level Error check is a runtime delta guard. At runtime a mutation that creates a new violation is rejected atomically; mutations that don’t make things worse pass, and pre-existing violations never block:

pub check OverweightTruck(v: Truck) :-
    v.weight > 100
    => Diagnostic { severity: Severity::Error, code: "Fleet::E001", /* … */ };

A check whose EDB is partly declared in source fires at both moments. Truck(ghost) is a declared fact, so UnweighedTruck fires once at build over the declared facts, and again at runtime on the observe channel for any truck registered without a weighing:

pub check UnweighedTruck(v: Truck) :- v: Truck, not Weighed(v) => Diagnostic { /* W002 */ };
pub fact Truck(ghost);

Running it

ox build discharges the build-moment checks and prints two warnings, then writes the artifact (warnings pass — a firing Error check would refuse the build):

Fleet::W001  type still specializes Deprecated — migrate it before v2   [OldTruck]
Fleet::W002  truck has never been weighed   [#i3356…]
wrote examples/check_constraints/target/root.oxbin

(W002’s subject is the declared ghost truck, rendered as its opaque individual id.)

ox run-scenario registers hauler at weight 50. The OverweightTruck Error guard passes (no new violation), and the observe channel still reports the pre-existing Fleet::W002 on the never-weighed ghost:

Fleet::W002  truck has never been weighed   [#i3356…]
scenario: applied 1 mutation(s) from examples/check_constraints/demo.toml

Registering a truck with weight > 100 would instead be refused atomically with Fleet::E001.

Honest caveats (what runs today)

• ox check --codes prints only error-severity codes (it is the machine-readable feed for the coverage gates). Both checks here that fire at build are Warnings, so --codes reports ok and exits 0 — the warnings surface on plain ox build (rendered) and on the run-scenario observe channel, not in the --codes stream.
• Catalog-level discharge happens at ox check / ox build; surfacing it live in the editor via the LSP is tracked follow-on work.

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the runtime delta-guard behaviour — the under-limit registration commits and an over-limit one is refused — so the both-moments discharge can’t drift from the language.

Defeated defeaters: a pardon restores the vote

Area: Defeasible reasoning Teaches: a defeater that is itself a #[default] and is itself defeated. The attacker stops blocking its target on exactly the tuples where the attacker was defeated — RFD 0028 D4, “defeated defeaters are legal.” Prerequisites: strict vs default vs defeater, lex specialis. Run: ox build examples/defeasible_defeated_defeater_v0 then ox run-scenario examples/defeasible_defeated_defeater_v0 --scenario <scenario.toml> (see Running it for a four-person scenario).

The previous examples have a two-level defeat: a default, and an attacker that blocks it. Here there are three levels — an exception, and an exception to the exception:

adult(p)         →  can_vote(p)              the overridable default
disenfranchised  ⇒  defeats can_vote          felons lose the vote
restored         ⇒  defeats disenfranchised   a pardon restores it

The legal question: a felon is disenfranchised, but a pardon overturns the disenfranchisement. Does the pardoned felon vote? The answer requires the middle rule to be both an attacker (of can_vote) and a target (of restored).

What to read in franchise.ar

The default and its attacker — but the attacker is itself a #[default], so it can be defeated in turn:

#[default]
#[label(adult)]
pub derive can_vote(p) :- Adult(p);

#[default]
#[label(felon)]
#[defeats(can_vote.adult(p))]
pub derive disenfranchised(p) :- Felon(p);

The exception to the exception. restored defeats disenfranchised’s labeled clause for the pardoned felons:

#[defeats(disenfranchised.felon(p))]
pub derive restored(p) :- Pardoned(p);

The subtle part is what disenfranchised is allowed to block. It blocks can_vote only on the felons it itself still survives for — i.e. the unpardoned ones. On a pardoned felon, disenfranchised is defeated, so it no longer blocks can_vote, and the adult default underneath survives. Resolving this correctly means resolving attacker survival in defeat-graph order, not from each attacker’s raw support.

Running it

This package ships no data (no demo.toml, no facts) — its behavior is exercised by registering people, so supply a four-person scenario. Save this as scenario.toml:

[[mutate]]
path = "franchise::register"
args = { p = "adam", age = 40, felon = false, pardoned = false }
[[mutate]]
path = "franchise::register"
args = { p = "ben", age = 30, felon = true, pardoned = false }
[[mutate]]
path = "franchise::register"
args = { p = "cleo", age = 50, felon = true, pardoned = true }
[[mutate]]
path = "franchise::register"
args = { p = "dot", age = 12, felon = false, pardoned = false }

Then ox run-scenario examples/defeasible_defeated_defeater_v0 --scenario scenario.toml:

adam   adult, not felon            → can_vote   (default, unattacked)
ben    adult, felon, NOT pardoned  → blocked    (disenfranchised survives)
cleo   adult, felon, PARDONED      → can_vote   (defeater itself defeated)
dot    minor                       → absent     (not an Adult)

so voters returns 2 rows — adam and cleo. The decisive contrast is ben vs cleo: both are felons, both are disenfranchised, but cleo’s disenfranchisement is itself defeated by the pardon, so the adult default underneath survives for her and not for ben.

This example is compiled and run in CI; the {adam, cleo} voter set — proving the pardoned felon votes and the unpardoned one stays blocked — is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), which registers the four people directly, so the defeated-defeater resolution can’t drift.

Recursion under a live defeat plane

Area: Defeasible reasoning Teaches: a recursive rule (transitive closure) still computes its full fixpoint when the module also carries a defeat plane — the defeasibility transform attributes each clause’s contribution over the converged support, so a recursive clause sees its own prior tuples. Prerequisites: lex specialis, and recursive derive rules (transitive closure). Run: ox build examples/defeasible_recursion_v0 && ox derive examples/defeasible_recursion_v0 reach

The presence of a single #[default]/#[defeats] pair anywhere in a module switches its entire evaluation onto the Governatori defeasibility transform rather than the classical Datalog fast path. A recursive rule must keep working under that transform. This example pins that property: a transitive closure, evaluated next to an unrelated defeat plane, must still be whole.

What to read in graph.ar

A standard recursive transitive closure over a 3-edge chain a → b → c → d:

pub derive reach(x: Node, y: Node) :- edge(x, y);
pub derive reach(x: Node, z: Node) :- reach(x, y), edge(y, z);

The recursive clause feeds on its own prior output — (a,c) needs (a,b) and (b,c) to already be in reach.

An unrelated defeat plane — a #[default] head attacked by a #[defeats] edge — on a different predicate entirely. Its only job here is to make has_defeat_plane() true so the whole module evaluates through the defeasibility transform:

#[default]
#[label(presumed)]
pub derive flagged(n: Node) :- Node(n);

#[defeats(flagged(n))]
pub derive cleared(n) :- edge(n, n);

cleared requires a self-loop edge(n, n); the chain has none, so the defeat never actually fires. It exists purely to activate the transform that the recursive closure must survive.

Running it

The graph is shipped as pub fact data (no mutations), so the runner is ox derive … reach rather than a scenario. Over a → b → c → d the closure is the six reachable pairs:

derive(reach): 6 tuple(s)
  (a,b) (a,c) (a,d)
  (b,c) (b,d)
  (c,d)

The transitive pairs (a,c), (b,d), (a,d) are exactly the ones the recursive clause derives from reach’s own prior tuples — the contributions a naive per-clause defeat attribution would drop if it cleared the head before attributing support. Six tuples, not three: the closure is whole under the live defeat plane.

This example is compiled and run in CI; the full six-pair closure under the defeat plane is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so a regression in the defeasibility transform breaks the build rather than silently under-deriving.

Legal norms: strict vs default vs defeater

Area: Defeasible reasoning Teaches: the three rule strengths of defeasible reasoning on one head — a strict (unattackable) clause, an overridable #[default] clause, and a #[defeats] directive that attacks the default per-tuple. RFD 0028’s “honest heads”: no rule spells the conclusion it denies. Prerequisites: refinement (iff/where), and derive rule bodies (see first-class relations). Run: ox build examples/legal_norms_can_vote && ox run-scenario examples/legal_norms_can_vote

Who can vote? Three norms speak to can_vote, and they conflict. A pre-defeasibility data language forces you to fold the exceptions into the rule body by hand (Adult(p), not Felon(p), not …), which becomes unmaintainable as exceptions accumulate. Argon keeps each norm a separate honest rule and resolves the conflict with directives.

What to read in norms.ar

The strict clause is unmarked — it is unattackable. Special-class members vote regardless of any disenfranchisement edge:

pub derive can_vote(p) :- SpecialClass(p);

The default clause is overridable. Adults vote by default — #[default] marks the clause as defeasible, and #[label(adult)] gives it an identity an attacker can name:

#[default]
#[label(adult)]
pub derive can_vote(p) :- Adult(p);

The exception is its own honest rule, and the attack is a directive. disenfranchised reads true on its own terms — it does not spell not can_vote. The attack lives in #[defeats(can_vote(p))], a meta-level statement about rules that resolves per-tuple against the bound p:

#[defeats(can_vote(p))]
pub derive disenfranchised(p) :- Felon(p);

So for a given person, disenfranchised defeats the default can_vote clause — but the strict clause is not a default, so the attack cannot touch it.

Running it

The scenario registers four people, one per case:

alice  age=25  felon=false  special=false  → can_vote   (default holds, unattacked)
bob    age=12  felon=false  special=false  → not        (not an Adult — no clause fires)
carol  age=30  felon=true   special=false  → not        (default defeated by disenfranchised)
dave   age=45  felon=true   special=true   → can_vote   (strict clause; the attack can't reach it)

so voters returns 2 rows — alice (default survives) and dave (strict overrides the very defeat that blocks carol). The decisive contrast is carol vs dave: both are felons, both are disenfranchised, but dave’s vote comes from the strict clause that #[defeats] cannot attack.

This example is compiled and run in CI; its can_vote extent under the strict/default/defeater interplay is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the resolution can’t drift from the language.

Defeat plane + check, in one module

Area: Defeasible reasoning Teaches: a #[defeats] lex-specialis priority plane and a check compliance invariant composing in the same build — a check evaluates over the warranted (post-defeat) extent, so a defeated conclusion never trips it. Prerequisites: lex specialis, and check invariants (see check constraints). Run: ox build examples/legal_obligations_compose_v0 && ox run-scenario examples/legal_obligations_compose_v0

A realistic legal consumer wants both: a vocabulary’s free compliance checks and defeasible norm priority. These were once mutually exclusive — ox build refused any module carrying both a check and a #[defeats]/#[default] plane, because the static-discharge evaluator ran the strict path only and would over-fire checks on conclusions the defeat plane removes. The fix composes them on a single principle: a check is a constraint over what the program concludes, and under a defeat plane the conclusions are the warranted, post-defeat extent.

What to read in statute.ar

A lex-specialis defeat plane — the general breach norm, defeated by a force-majeure exemption per-tuple:

#[default]
#[label(general)]
pub derive obligated(o) :- Outstanding(o);

#[defeats(obligated.general(o))]
pub derive exempt(o) :- ForceMajeure(o);

A check that reads the defeasible head. UnreviewedBreach fires on an obligation that is in breach but not reviewed. It reads the warranted obligated, so it must not fire on an exempted obligation — even though that obligation is still Outstanding (the general clause’s body):

pub check UnreviewedBreach(o: Obligation) :-
    obligated(o),
    o.reviewed == false
    => Diagnostic { severity: Severity::Error, code: "Compliance::E001", … };

A transitive downstream rule joins the defeasible head. seriousBreach is a non-defeasible rule that joins obligated — it must see the warranted extent, so it does not classify a defeated (exempted) obligation as serious even when that obligation is high-value. A second check, UnescalatedSeriousBreach, reads seriousBreach, so the defeated tuple must not leak through the downstream join into a check either:

pub derive seriousBreach(o) :- obligated(o), o.highValue == true;

This is the retraction-safe path: the warranted obligated is what every downstream consumer — checks and joins alike — observes.

Running it

The scenario opens three obligations:

ob1  outstanding, not force-majeure, reviewed     → breach, no violation
ob2  outstanding, FORCE MAJEURE (exempt), UNreviewed, high-value → defeated out of obligated
ob3  outstanding, not force-majeure, reviewed     → breach, no violation

The queries report:

query statute::breaches:        2 row(s)   — warranted obligated = { ob1, ob3 }
query statute::exemptions:      1 row(s)   — { ob2 }
query statute::seriousBreaches: 0 row(s)   — no high-value warranted breach

ob2 is both force-majeure and high-value, yet it appears in neither breaches nor seriousBreaches: the defeat removes it from obligated, and that removal propagates through the downstream join. ob2 is also the one unreviewed obligation — and yet UnreviewedBreach never fires on it, precisely because the check reads the warranted obligated and the defeat already removed ob2 from it (ob1 and ob3 are reviewed, so they trip nothing either). So the scenario commits cleanly — and the reason is the lesson: a module carrying both a defeat plane and a check now builds, and the check sees only the post-defeat extent.

Honest caveats (what runs today)

• The check’s firing behavior over the warranted extent — that UnreviewedBreach fires on an unreviewed warranted breach and does not fire on the exempted (defeated-away) obligation, and likewise for the transitive seriousBreach/UnescalatedSeriousBreach chain — is exercised by separate corpus tests with unreviewed obligations, not by this clean scenario. The scenario shows the module building and running; the corpus tests show the check discriminating.

This example is compiled and run in CI; the warranted breach extent and the check-firing behavior over it (including the transitive downstream relation) are pinned by corpus tests (oxc-runtime/tests/examples_corpus.rs), so the defeat↔check composition can’t drift.

Lease obligations: lex specialis as stratified negation

Area: Defeasible reasoning Teaches: expressing lex specialis (a specific exemption overriding a general breach norm) with stratified negation rather than the #[defeats] directive plane — the form you reach for when a module also imports a check-bearing vocabulary. Plus a real breach calculus over an imported deontic vocabulary. Prerequisites: lex specialis via #[defeats], defeat plane + check, and cross-package vocabulary (use legal_vocab_v0::…). Run: ox build examples/legal_obligations_v0 && ox run-scenario examples/legal_obligations_v0

This is the flagship legal-obligations model: a lease creates a rent obligation running from a tenant (debtor) to a landlord (creditor), declared against the separate legal_vocab_v0 deontic vocabulary. An obligation past its due date and unperformed is in breach — unless a force-majeure exemption applies. That “unless” is lex specialis again, but written a different way than the previous two examples, and the why is the lesson.

What to read in lease.ar

Lex specialis as stratified negation. The general breach norm fires unless the specific exemption holds; the exemption lives in a strictly-lower stratum, so not exempt(o) is well-defined:

pub derive outstanding(o) :- o: RentObligation, o.performed == false, o.due < today();
pub derive exempt(o)      :- o: ExemptObligation, outstanding(o);
pub derive breach(o)      :- outstanding(o), not exempt(o);

The resolution is identical to the #[defeats] lex-specialis in legal_priority_v0 — the specific rule wins for exactly the exempt obligations — but expressed with negation instead of a defeat directive.

Why not #[defeats] here? This package imports the check-bearing legal_vocab_v0, and ox build refuses any module that has both a check and a #[defeats]/#[default] plane in scope (check-discharge runs the strict path only). So when a defeat plane and an imported check can’t coexist in one build, stratified negation gives the same lex-specialis resolution and composes with the vocabulary’s catalog checks. (The composing case — defeat plane and check in one module, post-fix — is legal_obligations_compose_v0.)

A second, additive breach path for a long-stale obligation, still subtracting the exemption:

pub derive breach(o) :-
    o: RentObligation, o.performed == false, not exempt(o),
    o.due + 365.days < today();

The force-majeure exemption protects the obligor on this path too — it is not unconditionally overridden by staleness.

A derived penalty value bound in the rule head, rate × days-late, staying in the exact numeric tower:

pub derive penaltyOwed(o, amount) :- breach(o), amount = o.rate * o.daysLate;

Running it

The scenario opens four obligations against an evaluation clock of “today”:

ob1  due 2020-01-01, unperformed, NOT exempt   → breach (long-overdue path keeps it in at every clock)
ob2  due 2026-05-01, unperformed, EXEMPT        → not in breach (lex specialis subtracts it)
ob3  due 2026-05-01, unperformed, NOT exempt    → breach (outstanding, not exempt)
ob4  due 2026-05-01, PERFORMED                   → not in breach (discharged)

The queries report:

query lease::outstanding_obligations: 3 row(s)   — { ob1, ob2, ob3 }   (ob4 performed)
query lease::exempt_obligations:      1 row(s)   — { ob2 }
query lease::breached_obligations:    2 row(s)   — { ob1, ob3 }        (ob2 exempt; ob4 performed)
query lease::penalties:               2 row(s)   — (ob1, 1500) and (ob3, 250)

ob2 is outstanding but exempt, so the exemption subtracts it from breach on both paths — the lex-specialis point. The penalties are rate × daysLate: ob1 is 50.00 × 30 = 1500, ob3 is 25.00 × 10 = 250, both exact Decimal × Int.

Honest caveats (what runs today)

• #[defeats] and check are mutually exclusive in one build (the wall this model documents). The canonical RFD 0028 spelling of lex specialis is the #[defeats] directive plane, proven standalone in legal_priority_v0; it cannot be used here because this package imports a check-bearing vocabulary. Stratified negation is the composing form.
• Days-late is recorded, not computed from the dates. A penalty cannot be derived from elapsed time inside a rule: there is no Duration → Int day-count extractor, and today()/now() as a rule-body operand is refused with OE1316. So daysLate is stamped as an Int at breach time (recordBreach) rather than computed from today() - due.

This example is compiled and run in CI; the breach calculus over the cross-package vocabulary — the {ob1, ob3} breach extent and the 1500/250 penalties — is pinned by a CLI-pipeline test (oxc-driver/tests/cli_pipeline.rs), so the lex-specialis-via-negation behavior can’t drift.

Lex specialis: the specific rule defeats the general

Area: Defeasible reasoning Teaches: resolving a same-strength norm conflict with #[defeats] — lex specialis, where a specific rule beats the general one it names, per-tuple, by an explicit checked edge rather than a pair of magic priority integers. Prerequisites: strict vs default vs defeater. Run: ox build examples/legal_priority_v0 && ox run-scenario examples/legal_priority_v0

Two norms conclude about the same head at the same strength: imported goods owe import duty (general); medical imports are exempt (specific). Without a superiority mechanism this conflict is unresolvable — both fire on a medical import and you get a contradiction. Lex specialis is the legal rule that the specific norm wins; Argon expresses it as one rule defeating another’s labeled clause.

What to read in statute.ar

The general norm is an overridable, labeled default. #[label(general)] is the handle a more specific rule will name:

#[default]
#[label(general)]
pub derive must_pay_duty(g) :- Imported(g);

The specific norm names the general clause and defeats it. The #[defeats] target is qualified by the label — must_pay_duty.general(g) — and resolves per-tuple against the bound g. It defeats the general duty clause for exactly the goods exempt derives, and no others:

#[defeats(must_pay_duty.general(g))]
pub derive exempt(g) :- MedicalGood(g);

This is the whole lex-specialis idea in two lines: the more specific rule (medical imports) defeats the more general one (imported goods), tuple by tuple. A non-medical import is untouched by the defeat and keeps owing duty.

Running it

The scenario declares four goods:

steel    imported=true   medical=false  → owes duty   (general default, unattacked)
insulin  imported=true   medical=true   → exempt      (specific defeats general)
gauze    imported=true   medical=true   → exempt      (specific defeats general)
widget   imported=false  medical=false  → no clause fires

so dutiable (the warranted must_pay_duty) returns 1 row — steel — while exemptions returns 2 rows, insulin and gauze. The two medical imports are dutiable under the general norm and exempt under the specific one; lex specialis subtracts them from the duty extent, leaving the single non-medical import.

This example is compiled and run in CI; the post-defeat must_pay_duty and exempt extents are pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the lex-specialis resolution can’t drift.

Federation: the DEFAULT layer joins as a constituent

Area: Standpoints & federation Teaches: the DEFAULT (unscoped) layer is not a privileged outer frame that overrides standpoints — it is a join constituent on equal footing. Because the DEFAULT layer restricts into every scoped view, a DEFAULT-asserted fact and a scoped refutation of the same individual collide inside one standpoint’s view, and the four-valued join yields both. Prerequisites: standpoint visibility and federation: when standpoints disagree. Run: ox build examples/federation_default_conflict && ox query examples/federation_default_conflict --with-truth4

The visibility example showed that a DEFAULT-layer fact restricts into every view — its agreement case. This example pins the disagreement case, and it is the subtle one. A single standpoint’s view is DEFAULT ∪ own. So when DEFAULT asserts a fact and the standpoint refutes it, both polarities live in the same view, and the information-join produces both — even though only one standpoint is federated. DEFAULT does not win by virtue of being the base; it participates in the join like any other source.

What to read in conflict.ar

One standpoint, with DEFAULT-layer facts above it:

pub type Person;

pub standpoint s;

// DEFAULT-layer (unscoped) facts — restrict into the scoped view `s`.
pub fact Person(eve);
pub fact Person(frank);

The standpoint refutes one of the DEFAULT facts, and refutes a third individual DEFAULT is silent on:

pub standpoint s {
    // `s` refutes the DEFAULT-layer `eve` — a same-view collision → Both.
    pub not_fact Person(eve);
    // `s` refutes `gwen`, on whom DEFAULT is silent → Not.
    pub not_fact Person(gwen);
}

Federating over the single standpoint still meets the DEFAULT layer — s’s view is DEFAULT ∪ s:

pub query conflicting() -> Person across [s];

Running it

Even across a single standpoint, the DEFAULT layer is a constituent, so the join surfaces three different verdicts:

eve    → Both   (DEFAULT asserts Person, s refutes — both meet in s's view)
frank  → Is     (DEFAULT asserts, s silent)
gwen   → Not    (s refutes, DEFAULT silent)

The decisive row is eve → Both. There is only one standpoint in across [s], so it is tempting to read DEFAULT as an outer context that s overrides — it is not. The DEFAULT assertion of eve and s’s refutation of eve are two constituents of one join, and the join holds both. Contrast frank (Is — DEFAULT alone) and gwen (Not — s alone): the verdict is exactly the information-join of whatever each layer contributes, with DEFAULT counted, never privileged.

Honest caveats (what runs today)

• This is the same paraconsistent federation policy as the two-source case: collisions are preserved as Both, not resolved in DEFAULT’s favor.
• Rows are reported by individual id; the name mapping above is how the package declares its facts.

This example is compiled and run in CI; the DEFAULT-disagreement verdicts (eve = Both in particular) are pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the equal-footing join rule can’t drift.

Federation: when standpoints disagree

Area: Standpoints & federation Teaches: across [...] joins standpoints by the four-valued information-join (FDE / Truth4). When two sources speak to the same individual, the join surfaces all four values — is, not, can, and crucially both, which arises only from one source asserting while another refutes. Prerequisites: standpoint visibility (DEFAULT vs scoped facts). Run: ox build examples/federation_disagreement && ox query examples/federation_disagreement --with-truth4

Two data sources rarely agree on everything. Most systems force you to pick a winner or crash on the conflict. Argon does neither: it federates them and reports the disagreement as a value. The four-valued truth space — is (asserted), not (refuted), can (neither), both (asserted and refuted) — is a bilattice, and across [...] combines standpoints by the information-join over it. A conflict does not corrupt the answer; it becomes both.

What to read in federation.ar

Two standpoints, each its own source of truth:

pub type Person;

pub standpoint historical;
pub standpoint public_record;

One source asserts with fact; the other refutes with not_fact (strong negation):

pub standpoint historical {
    pub fact Person(alice);
    pub fact Person(bob);
}

pub standpoint public_record {
    pub not_fact Person(alice);
    pub not_fact Person(carol);
    pub fact Person(dave);
}

not_fact is not absence — it is a positive refutation. historical says alice is a Person; public_record says alice is not. They overlap on alice and clash.

The federated query joins both sources:

pub query everyone() -> Person across [historical, public_record];

Running it

The query returns one row per individual, each tagged with the joined four-valued status:

alice  → Both   (historical asserts Person, public_record refutes)
bob    → Is     (only historical asserts)
carol  → Not    (only public_record refutes)
dave   → Is     (only public_record asserts)

All four Truth4 values appear in a single query. The decisive row is alice → Both: she is the only individual both asserted (by historical) and refuted (by public_record), and the information-join carries both polarities rather than discarding either. bob and dave are Is because exactly one source asserts and nothing refutes; carol is Not because she is refuted with no countervailing assertion. The can value is the join’s bottom — neither asserted nor refuted — and is what an individual no source mentions would read.

Honest caveats (what runs today)

• This is the default paraconsistent federation policy: a conflict is preserved as Both rather than resolved or rejected. A source declaring a contradiction does not poison the whole query.
• Rows are reported by individual id; the name mapping above is how the package declares its facts.

This example is compiled and run in CI; the per-row Truth4 verdicts under federation are pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the information-join can’t drift from the language.

Standpoint visibility: the DEFAULT layer vs scoped facts

Area: Standpoints & federation Teaches: how a fact’s scope decides which views can see it. A DEFAULT-layer (unscoped, module-level) fact restricts into every view; a standpoint-scoped fact is local to its standpoint. This is the sheaf reading of visibility — a global section restricts to every open set; a local section does not. Prerequisites: concepts, and pub query (see first-class relations). Run: ox build examples/standpoint_visibility && ox query examples/standpoint_visibility --with-truth4

A standpoint is a named viewpoint — a place from which facts are asserted and read. Standpoints sit in a <: lattice, and the unscoped DEFAULT layer is the shared base every standpoint extends. The question this example answers: when you assert a fact, who can see it? The answer turns entirely on whether the fact is scoped.

What to read in visibility.ar

Two standpoints and one concept:

pub type Widget;

pub standpoint s1;
pub standpoint s2;

A DEFAULT-layer fact is unscoped — declared at module level, outside any standpoint block. It restricts into every view:

// DEFAULT-layer (unscoped) fact — visible in every view.
pub fact Widget(dfl);

A scoped fact lives inside a standpoint block and is local to it:

pub standpoint s1 {
    pub fact Widget(only_s1);
}

pub standpoint s2 {
    pub fact Widget(only_s2);
}

Four queries read from four vantage points. The base query is unfederated (DEFAULT only); across [...] selects which standpoints join the view:

pub query base() -> Widget;                       // DEFAULT only
pub query in_s1() -> Widget across [s1];           // DEFAULT ∪ s1
pub query in_s2() -> Widget across [s2];           // DEFAULT ∪ s2
pub query fed() -> Widget across [s1, s2];         // DEFAULT ∪ s1 ∪ s2

Running it

The four views form a visibility matrix — dfl is the DEFAULT-layer individual, only_s1/only_s2 are scoped:

base   (unfederated):   { dfl }                    — DEFAULT only
in_s1  (across [s1]):    { dfl, only_s1 }           — DEFAULT ∪ s1
in_s2  (across [s2]):    { dfl, only_s2 }           — DEFAULT ∪ s2
fed    (across [s1, s2]): { dfl, only_s1, only_s2 } — DEFAULT ∪ s1 ∪ s2

The decisive cell is only_s1 against base and in_s2: it is invisible to both. A standpoint-scoped fact does not leak into the unfederated base view, and it does not leak into a different standpoint’s view. Seeing it requires explicitly selecting s1 (or federating over a list that includes it). Meanwhile dfl appears in all four rows — the DEFAULT layer is the floor every view stands on.

Every row reads [Is] here: there is no disagreement in this example, so the four-valued status is uniform. (For where [Both] arises, see federation: standpoints disagree and federation: the DEFAULT layer joins as a constituent.)

Honest caveats (what runs today)

• The query output identifies rows by individual id; the named mapping above (dfl, only_s1, only_s2) is how the package declares them.
• --with-truth4 surfaces the per-row four-valued tag. Unfederated queries always read Is; the federated views here also read Is because nothing refutes a Widget.

This example is compiled and run in CI; the four-quadrant visibility matrix is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so a leak across standpoints breaks the build rather than the docs.

Effective dating: which rate is in force on a date

Area: Bitemporal time Teaches: the valid-time axis — insert iof(…) at #date# writes a fact whose effectivity begins on a civil date, and as_of <#date#> reads which facts were in force on a given day. This is distinct from (and composable with) the transaction-time as_of <int> of temporal_as_of_surface. Prerequisites: as_of time-travel, and first-class relations. Run: ox build examples/effective_dated_tax_v0 && ox run-scenario examples/effective_dated_tax_v0

“What was the standard tax rate on 2024-04-15?” is a valid-time question: it asks what was true in the world on that day, not what the system happened to know at some processing instant. Hand-rolling an effectiveFrom: Date field forces every query to re-implement interval logic. Argon puts effectivity on the substrate: an enactment is written at its effective date, and a date-stamped as_of read projects the rates in force.

What to read in tax.ar

StandardRate is “the standard rate in force”; each enactment is one individual, and its value rides on a rate relation tuple. The enactment writes both at the effective date, so before that date neither holds:

pub type StandardRate;
pub rel rate(r: StandardRate, pct: Decimal);

pub mutate enact(r: StandardRate, pct: Decimal, effective: Date) {
    insert iof(r, StandardRate) at effective;
    insert rate(r, pct) at effective;
}

The queries read the valid-time axis with a date-literal as_of:

pub query rate_on_2023_06_01() -> StandardRate as_of #2023-06-01#;
pub query rate_on_2024_04_15() -> StandardRate as_of #2024-04-15#;
pub query rate_on_2025_06_01() -> StandardRate as_of #2025-06-01#;
pub query rate_now()           -> StandardRate;

Running it

The demo.toml enacts three rates — 20% effective 2020-01-01, 22% effective 2024-01-01, 19% effective 2025-01-01 — passing the Date and Decimal arguments in their exact table forms ({ date = "…" }, { decimal = "…" }). Each date-stamped query then projects the rates whose valid-time has begun by that day:

query tax::rate_on_2023_06_01:  1 row(s)   — only the 2020 rate has begun
query tax::rate_on_2024_04_15:  2 row(s)   — 2020 + 2024 are both in force by a 2024 filing
query tax::rate_on_2025_06_01:  3 row(s)   — 2020 + 2024 + 2025
query tax::rate_now:            3 row(s)   — every begun rate (valid = now)

The decisive contrast is rate_on_2023_06_01 vs rate_on_2024_04_15: the same query shape, two civil dates, and the row count rises from 1 to 2 because the 2024 enactment’s valid-time interval opens between them. A rate enacted at #2024-01-01# is invisible to a 2023 read and visible to a 2024 read — the effectivity is enforced by the substrate, not by a where clause in the query.

Honest caveats (what runs today)

• The rate table is append-only in this v0: each enactment opens a valid-time interval but does not close the prior one, so a later date sees all begun rates accumulated (hence 3 rows in 2025), not only the single rate that superseded. Closing the prior interval (so a date sees exactly one rate) is the during / bitemporal-retraction follow-on.
• Date arguments use the { date = "…" } table form (a bare string parses as an individual); Decimal arguments use { decimal = "…" }, parsed exactly rather than through a float.
• This is the valid-time axis (true-in-the-world). It composes with — and is distinct from — the transaction-time axis of temporal_as_of_surface (when the system learned a fact).

This example is compiled and run in CI; its valid-time as_of <#date#> round-trip is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the effective-dating surface can’t drift from the language.

Time-travel: as_of reads the past

Area: Bitemporal time Teaches: the surface as_of clause on a pub query — the same query, snapshotted at different transaction-times, returns different answers. Every mutation stamps a monotonic transaction-time, and as_of <tx> reads the state visible at that instant. Prerequisites: refinement (iff), and mutate bodies. Run: ox build examples/temporal_as_of_surface && ox run-scenario examples/temporal_as_of_surface

A database that only knows “now” cannot answer “what did we believe last Tuesday”. Argon’s substrate is bitemporal: each mutation emits events with a monotonically-increasing transaction-time stamp, and a query can read as of any past stamp. The history is queryable, not overwritten.

What to read in chronicle.ar

A Person carries a mutable age, and Adult is the iff-refinement that classifies anyone 18 or older:

pub type Person { mut age: Int }
pub type Adult <: Person iff { self.age >= 18 };

Two declared queries pin the same Adult extent to two past transaction-times — the surface as_of <int> clause is the whole point:

pub query current_adults() -> Adult;          // latest snapshot
pub query adults_at_2()    -> Adult as_of 2;   // right after the hire
pub query adults_at_4()    -> Adult as_of 4;   // right after set_age

The driver routes a query carrying as_of through the time-travel read path automatically; the modeler never touches the runtime API.

Running it

The demo.toml scenario hires alice as a minor (age 12), then later sets her age to 25. Each mutation advances transaction-time, so the same Adult query gives different answers at different stamps:

query chronicle::adults_at_2:   0 row(s)        — alice is 12 here, not an Adult
query chronicle::adults_at_4:   1 row(s)  alice — alice is 25 here, now an Adult
query chronicle::current_adults: 1 row(s) alice — latest state agrees with tx=4

The decisive contrast is adults_at_2 vs adults_at_4: it is one query against one individual, but the answer flips from empty to {alice} purely because the read snapshot moved past the set_age event. The refinement is re-evaluated against the field value as of each instant.

Honest caveats (what runs today)

• v0 admits only integer literals as the as_of argument (a raw transaction-time stamp). Forms like as_of now() - 1 day or a parameterized argument are reserved for a later RFD.
• This is the transaction-time axis (when the system learned a fact). The valid-time axis — when a fact is true in the modelled world — is shown in effective_dated_tax_v0, which reads as_of <#date#>.

This example is compiled and run in CI; its as_of snapshot behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the time-travel surface can’t drift from the language.

Time-travel: a refinement’s verdict changes over time

Area: Bitemporal time Teaches: how an iff-refinement composes with bitemporal time-travel — as a field rises across transaction-time, the individual’s membership in the refinement changes per snapshot. The classifier is re-run against the field value as of each instant. Prerequisites: as_of time-travel, and refinement (iff). Run: ox build examples/temporal_promotion && ox run-scenario examples/temporal_promotion

In temporal_as_of_surface the query moved through time. Here the classification moves: an employee crosses a threshold, and the refinement that depends on that field flips from non-member to member — but only for snapshots taken after the crossing.

What to read in hr.ar

FullTime is the iff-refinement over an employee’s weekly hours:

pub type Employee { mut weekly_hours: Int }
pub type FullTime <: Employee iff { self.weekly_hours >= 35 };

pub query all_employees() -> Employee;
pub query full_timers()   -> FullTime;

There is no as_of on these declared queries; the time-travel here is driven by the --as-of flag on ox query, which reads the FullTime extent visible at a chosen transaction-time.

Running it

The demo.toml scenario hires alice at 20 hours/week (below the threshold), then promotes her to 40. The latest snapshot has her full-time:

$ ox run-scenario examples/temporal_promotion
query hr::all_employees: 1 row(s)  alice
query hr::full_timers:   1 row(s)  alice      — 40 >= 35 in the latest state

Travel back, and the verdict flips. The same FullTime extent, read at different transaction-times:

$ ox query examples/temporal_promotion --extent hr::FullTime --as-of 1
extent(hr::FullTime as_of 1): 0 individual(s)             — alice still at 20h, not FullTime

$ ox query examples/temporal_promotion --extent hr::FullTime --as-of 100
extent(hr::FullTime as_of 100): 1 individual(s)  alice    — past the promotion, 40 >= 35

The decisive contrast is --as-of 1 vs --as-of 100: one individual, one refinement, two snapshots — empty before the promotion, {alice} after. The field value is read as of the same instant the membership is evaluated (the latest property assertion with tx_from <= tx wins per field), so the iff classifier sees 20 in the past and 40 in the present.

Honest caveats (what runs today)

• --as-of takes a transaction-time stamp as an integer. A stamp before any event (--as-of 1) reads the pre-promotion state; a large stamp (--as-of 100) reads the latest.
• The --as-of flag lives on ox query; ox run-scenario prints the latest snapshot for the declared queries.

This example is compiled and run in CI; the corpus test (oxc-runtime/tests/examples_corpus.rs::corpus_temporal_promotion_full_time_eligibility_changes_over_time) pins exactly this — the FullTime extent differing across transaction-time as the hours rise — so the refinement-over-time composition can’t drift.

Modal operators: box and diamond

Area: Modal operators Teaches: the necessity (box) and possibility (diamond) operators in a rule body, and v0.1’s rigid-default discharge — over a rigid type, both box(P) and diamond(P) reduce to P at the current world. The classifier promotes a rule carrying a modal operator to tier:modal. Prerequisites: concepts, and derive rule bodies (see first-class relations). Run: ox build examples/modal_box_diamond && ox derive examples/modal_box_diamond necessarily_eligible — this reads the empty store (0 tuple(s)); register a Citizen first to see the discharge (see Running it).

Modal logic distinguishes what must hold from what may hold. box(P) reads “necessarily P” — P at every accessible world; diamond(P) reads “possibly P” — P at some accessible world. Argon exposes both as operators usable inside a rule body. In v0.1 the semantics are rigid-default: for a rigid type — the UFO default, e.g. kind and struct — membership does not vary across worlds, so necessity and possibility both collapse to truth at the current world. This is the correct static-discharge answer for a rigid type, and conservative-degenerate for anti-rigid types until the Kripke evaluator lands.

What to read in governance.ar

One rigid type, wrapped in each operator by a separate rule:

pub type Citizen;

pub derive necessarily_eligible(p) :- box(Citizen(p));

pub derive possibly_eligible(p) :- diamond(Citizen(p));

box(Citizen(p)) and diamond(Citizen(p)) both discharge to p: Citizen because Citizen is rigid. The classifier promotes both rules to tier:modal, and the build admits them.

A mutation supplies the citizens, and two queries read the modal derives:

pub mutate register(p: Citizen) {
    insert iof(p, Citizen);
}

pub query who_necessarily_eligible() -> necessarily_eligible;
pub query who_possibly_eligible() -> possibly_eligible;

Running it

The package ships no seed facts, so against the empty store both derives are empty:

$ ox derive examples/modal_box_diamond necessarily_eligible
derive(necessarily_eligible): 0 tuple(s)

Membership comes from register. Registering one citizen (alice) and reading the two queries shows the discharge:

query who_necessarily_eligible: 1 row(s)   → alice
query who_possibly_eligible:    1 row(s)   → alice

Both queries return exactly alice, the registered Citizen — and nothing else. That is the whole point of rigid-default discharge: over a rigid type, box and diamond agree, and they agree with plain membership. An unregistered individual matches neither rule, since there is no iof(_, Citizen) for the modal body to discharge against.

Honest caveats (what runs today)

• v0.1 is rigid-default. box and diamond collapse to current-world truth. The full Kripke evaluator — where the two operators genuinely diverge over anti-rigid types — is future work; today the surface is wired and the discharge is sound for rigid types.
• The package ships no demo.toml, so a bare ox derive reads the empty store. To reproduce the rows above, register a Citizen first (the corpus test drives governance::register programmatically; from the CLI, a one-line scenario file with a [[mutate]] entry for governance::register does the same via ox run-scenario).

This example is compiled and run in CI; the rigid-default box/diamond discharge — both operators matching the registered Citizen and nothing else — is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs).

Trait contracts: clause union, supertraits, and reflective dispatch

Area: Traits Teaches: the trait atom — a rule-plane trait whose per-type impl clauses union under one head (dispatch is derivation), a supertrait acting as a requires-constraint, the partial-coverage guard that excludes uncovered individuals explicitly rather than by silence, enumeration/NAF over the catalog-closed $implements relation, and a #[static] conformance check. Prerequisites: concepts and <:; derive rule bodies; the reflective meta-plane (meta, implements, specializes). Run: ox build examples/trait_contracts && ox check --codes examples/trait_contracts — and ox derive examples/trait_contracts/target/root.oxbin ServiceableKinds

A trait names a contract a type can implement. Inspectable requires a Due rule; each impl Inspectable for T supplies one clause, and the clauses union under the single Inspectable::Due head. Dispatch is not a vtable lookup — it is derivation: the reasoner fires whichever clauses match.

What to read in fleet.ar

Clause union — one head, three type-guarded clauses with per-kind thresholds:

pub trait Inspectable { derive Due(Self); }
impl Inspectable for Truck { derive Due(t: Self) :- t.hours >= 100; }
impl Inspectable for Crane { derive Due(c: Self) :- c.hours >= 50; }
impl Inspectable for Drone { derive Due(d: Self) :- d.hours >= 10; }

A supertrait is a requires-constraint (Rust’s :): impl Serviceable for T demands impl Inspectable for T, and the reflective surface closes over it — implements(t, Serviceable) entails implements(t, Inspectable). Serviceable covers only Truck and Crane; Drone is field-maintained.

The partial-coverage guard (D3.2). A bare NeedsService(a) over Asset would be OE1327 because Serviceable does not cover every kind. ShopQueue writes the dispatch-can-fail branch explicitly — uncovered drone individuals are excluded by the guard’s $implements join, never by silence:

pub derive ShopQueue(a: Asset) :-
    implements(meta(a), Serviceable),
    NeedsService(a);

Enumeration and NAF over the catalog-closed $implements — these read type names directly, with no instances:

pub derive ServiceableKinds(t) :- implements(t, Serviceable);
pub derive SelfMaintained(t)  :- specializes(t, Asset), t != Asset, not implements(t, Serviceable);

A #[static] catalog-level conformance check discharges totally at ox check. It PASSES — the three Inspectable impls cover every declared asset kind:

#[static]
pub check EveryAssetKindIsInspectable(t: TypeRef) :-
    specializes(t, Asset), t != Asset, not implements(t, Inspectable)
    => Diagnostic { severity: Severity::Error, code: "Fleet::E010", /* … */ };

Running it

ox check discharges the catalog-level conformance check and passes — every asset kind is inspectable:

$ ox check --codes examples/trait_contracts
ok

The catalog-closed reflective derives need no instances, so ox derive reads them straight off the type catalog:

$ ox derive examples/trait_contracts/target/root.oxbin ServiceableKinds
derive(ServiceableKinds): 2 tuple(s)
  (fleet::Truck)
  (fleet::Crane)

$ ox derive examples/trait_contracts/target/root.oxbin SelfMaintained
derive(SelfMaintained): 1 tuple(s)
  (fleet::Drone)

ServiceableKinds = {Truck, Crane} (the free-t enumeration over implements(t, Serviceable)); SelfMaintained = {Drone} (the NAF complement). Once individuals are registered, InspectionQueue collects every asset past its kind’s threshold (truck 100h / crane 50h / drone 10h — the Inspectable cover is total), while ShopQueue admits only the guard-covered and clause-satisfying ones (the worn truck, the flagged crane) — never a drone, even a worn one: its dispatch fails visibly through the guard.

Honest caveats (what runs today)

• The package has no demo.toml, and the instance-driven derives (Due, InspectionQueue, ShopQueue) need registered individuals — ox derive over the bare artifact shows them empty. The catalog-closed reflective derives (ServiceableKinds, SelfMaintained) are the part demonstrable straight from the CLI; the instance-driven extents are pinned by the corpus test, which seeds via the register_* mutations.
• To see the failing conformance variant, retarget the check at Serviceable (commented in fleet.ar): Drone implements no Serviceable, so ox check fails with Fleet::E010 before any artifact is written.

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the clause-union InspectionQueue, the D3.2-guarded ShopQueue (truck + crane, never a drone), ServiceableKinds = {Truck, Crane}, SelfMaintained = {Drone}, and the check’s catalog-level classification, so the trait surface can’t drift from the language.

assert rejects: unit-testing that a constraint refuses bad data

Area: Testing Teaches: the negative-enforcement half of the test atom. Argon is a constraint language, so a model’s most important property is which writes its invariants turn away — assert rejects { … } runs a write block against an isolated world and PASSes when the write is refused. An optional (Pkg::Code) pins the exact rejecting code. Prerequisites: refinement (where invariants); check constraints (delta guards). Run: ox test examples/assert_rejects_v0

The positive test forms — assert <expr> and assert [not] derivable — say what a model accepts or derives. They cannot say what it refuses. assert rejects { <writes> } is the missing half: it runs its block against an isolated copy of the test world, and a write-path guard rejection is a PASS (the rejected transaction commits nothing). An accepted write FAILs; a non-guard error — a typo, an unbound name — ERRORs loudly and never masquerades as a passing rejection.

What to read

The constraints under test in model.ar: a where-invariant concept (membership asserted, balance >= 0 enforced at the write with OE0668) and a check delta-guard (a new over-100t truck refused with Fleet::E001):

pub type Solvent <: Account where { self.balance >= 0 };

pub check OverweightTruck(v: Truck) :-
    v.weight > 100
    => Diagnostic { severity: Severity::Error, code: "Fleet::E001", /* … */ };

The tests in tests/mod.ar exercise each rejection mode. A where-invariant violation, a code-pinned check rejection, the same rejection without a pin, and a legal write that must NOT satisfy a rejection assertion:

test "a negative balance is rejected by the where-invariant" {
    let a = insert Solvent { balance: 100 };
    assert rejects { update a: Account set { balance = -50 } };
}

test "an overweight truck is rejected by its check, by code" {
    assert rejects(Fleet::E001) { let t = insert Truck { weight: 200 }; };
}

test "a within-limit balance is accepted" {
    let a = insert Solvent { balance: 100 };
    update a: Account set { balance = 50 };
    assert a.balance == 50;        // the positive form tests an accepted write
}

Running it

ox test discovers every test "name" { … } block, runs each against a fresh store, and reports pass/fail/error (it exits non-zero if any fails or errors — CI-usable):

$ ox test examples/assert_rejects_v0
PASS  a negative balance is rejected by the where-invariant
PASS  an overweight truck is rejected by its check, by code
PASS  an overweight truck is rejected by its check
PASS  a within-limit balance is accepted

4 passed, 0 failed, 0 errored, 0 inconclusive

The decisive contrast is the last test against the first three: setting a Solvent account to -50 is refused by the where-invariant (so assert rejects passes), but setting it to 50 is accepted — and an accepted write is tested with the positive assert a.balance == 50, never with assert rejects. The code-pinned variant passes only on its exact code: assert rejects(Fleet::E001) would FAIL, not pass, if the write were turned away by some other guard.

Honest caveats (what runs today)

• assert rejects is satisfied by a write-path guard rejection (a where-invariant OE0668 or a check delta-guard). A non-guard error inside the block (an unbound name, a type error) is an ERROR, not a PASS — the form does not let a broken test launder itself into a green rejection.
• Each block runs against an isolated copy of the test world, so a rejected transaction leaves no residue for the next test.

This example is compiled and run in CI; a CLI test (oxc-driver/tests/cli_pipeline.rs) runs ox test examples/assert_rejects_v0 and asserts it stays green, and a companion test pins that the test runner classifies every outcome (pass / fail / error), so the negative-enforcement surface can’t drift from the language.

Residential lease: a breach / fulfillment calculus

Area: Capstone Teaches: the worked, end-to-end legal model — a UFO-L deontic theory of a residential lease where concepts, first-class relations, refined collections, mod structure, cumulative aggregation, and recursion-through-negation rules combine to decide, per obligation, whether it is breached or fulfilled as of a date. The capstone of the corpus. Prerequisites: first-class relations, refined collections and from-fields (see refined collections), derive rule bodies with aggregates and negation, and the in-package vocabulary pattern (pub metatype, see legal vocabulary). Run: ox build examples/residential_lease_breach && ox run-scenario examples/residential_lease_breach

This is the example the rest of the corpus builds toward. The others isolate one idea — a relation carries data, a #[defeats] plane resolves a conflict, a check reads a warranted extent. Here those ideas carry a single working legal model: a residential lease, transcribed faithfully from a propositional-content theory in the UFO-L tradition of Griffo/Guizzardi. The question the model answers is the one a lease actually poses — given what was owed, what was paid, and what day it is, which obligations are in breach? — and it answers it by running, not by hand-waving.

The package is two modules: root.ar (mod lease;) and lease.ar, which holds the whole hierarchy, the calculus, the seeding mutations, and the queries.

The UFO vocabulary is declared in-package, not built in

UFO’s classifiers are not Argon language surface. Even the std::core baseline type/rel is opt-in — this package’s ox.toml lists them in its prelude (RFD 0038 D4; the baseline is no longer ambient). A category/kind/relator introducer then resolves against pub metatype declarations visible in scope — an introducer with no visible declaration is refused (OE0605). The example declares the three UFO metatypes it uses locally — the external-vocabulary-package pattern, where a real UFO package authored with the UFO authors would ship these and be imported instead:

pub metatype category = { };   // a rigid non-sortal classifier
pub metatype kind     = { };   // a rigid sortal supplying an identity principle
pub metatype relator  = { };   // the truth-maker of material relations

Everything downstream is vocabulary, not keyword: pub category Endurant;, pub kind Person <: LegalAgent { name: String }, pub relator CorrelativePositionPair <: LegalRelator { … }. The compiler never reads the word “category” as special — it reads a metatype declared one screen up.

What to read in lease.ar

Cumulative tracking is built from records, accounts, and a book. A Record carries a value and a closed day-window [startsOn, endsOn]. An expected record says what is owed in a period; a satisfaction record says what was performed. An account holds records as a refined collection navigated through a relation — the from recordInAccount.range field is the collection of records reachable across that relation:

pub category Record { mut value: Real, mut startsOn: Int, mut endsOn: Int }
pub category RecordAccount { records: [Record] from recordInAccount.range }
pub rel recordInAccount(account: RecordAccount, record: Record);

A CorrelativePositionBook separates the two sides through bookExpectedAccount and bookSatisfactionAccount, so the calculus can compare what is owed against what was realized.

Legal positions are Hohfeldian relators. A right–duty pair is the truth-maker that links an advantaged holder, a burdened holder, the tracking book, and the propositional content that supplies its legal meaning. For rent the landlord is advantaged, the tenant burdened:

pub relator CorrelativePositionPair <: LegalRelator {
    advantageHolder: LegalAgent,
    burdenHolder: LegalAgent,
}
pub relator RightDutyPair <: CorrelativePositionPair;

The propositional content hierarchy is a named cover. The = A | B | … transcribes the source theory’s partition blocks — the alternatives are disjoint and exhaustive. A content is either an occurrence-referring content (positive or negative), a conditional, a conjunction, or a disjunction:

pub category PropositionalContent =
    OccurrenceReferringPropositionalContent |
    ConditionalPropositionalContent |
    Conjunction |
    Disjunction

Positive content is fulfilled by matching satisfaction (rent paid); negative content by the absence of a forbidden occurrence (no subletting). Conjuncts and disjuncts are refined collections too, with cardinality on the slot — a conjunction needs at least two conjuncts, a disjunction at most two disjuncts:

pub category Conjunction <: PropositionalContent {
    conjunct: [PropositionalContent; >= 2] from conjunctOf.range
}

The calculus is the set of derive rules. An expected record is Met when the cumulative realized value in its satisfaction account covers the expected value — a sum aggregate over the navigated collection:

pub derive Met(e: ExpectedSatisfactionRecord) :-
    recordInAccount(expectedAccount, e),
    bookExpectedAccount(book, expectedAccount),
    bookSatisfactionAccount(book, satisfactionAccount),
    e.value <= sum(r.value for r in satisfactionAccount.records);

Breach is as of an instant. PastCurrent(e, t) holds when e’s window has closed on or before t (the obligation is due, so non-satisfaction now counts). Positive content is breached as of t when a past-due expected record is not Met — negation over the aggregate-defined Met:

pub derive BreachedAt(pc: PositiveOccurrencePropositionalContent, t: Instant) :-
    contentBook(pc, book),
    bookExpectedAccount(book, expectedAccount),
    recordInAccount(expectedAccount, e),
    PastCurrent(e, t),
    not Met(e);

Fulfillment is the negation of breach, and composition is per the deontic logic. Positive content is fulfilled as of t when it is not BreachedAt; a conjunction is breached when any conjunct is breached (existential), and a disjunction is fulfilled when at least one disjunct is fulfilled:

pub derive Fulfilled(pc: PositiveOccurrencePropositionalContent, t: Instant) :-
    PositiveOccurrencePropositionalContent(pc), Instant(t), not BreachedAt(pc, t);

pub derive BreachedAt(conj: Conjunction, t: Instant) :- conjunctOf(conj, c), BreachedAt(c, t);
pub derive Fulfilled(disj: Disjunction, t: Instant) :- disjunctOf(disj, d), Fulfilled(d, t);

Each a.b.c navigation in the source theory becomes one join per hop over the relation that is that navigation (contentBook, bookExpectedAccount, …) — semantically identical, and how the relations materialize anyway.

Running it

The harness sets the clock to day 45 and opens three rent obligations, each €1000 due on day 31 (so all are past-due as of day 45). They differ only in what was paid, plus two composites over { rentPaid, rentUnpaid }:

rentUnpaid   paid 0           → not met → BREACHED   as of day 45
rentPaid     paid 600 + 400   → met     → FULFILLED  as of day 45
rentPartial  paid 600         → not met → BREACHED   as of day 45
bothRents    (rentPaid AND rentUnpaid)  → BREACHED   (one conjunct breached)
eitherRent   (rentPaid OR  rentUnpaid)  → FULFILLED  (one disjunct fulfilled)

ox run-scenario applies the nine mutations and reports the three query extents (individual ids elided; the subjects are named here for reading):

scenario: applied 9 mutation(s) from examples/residential_lease_breach/demo.toml
query lease::breached: 3 row(s)   — { rentUnpaid, rentPartial, bothRents } each as of `today`
query lease::fulfilled: 2 row(s)  — { rentPaid, eitherRent } each as of `today`
query lease::met: 1 row(s)        — { expPaid }  (the only fully-covered expected record)

The decisive reads: rentPartial is breached even though €600 was paid, because cumulative satisfaction (600) does not cover the expected 1000 — the sum-defined Met fails and not Met fires. rentPaid is met because 600 + 400 = 1000 covers it, so BreachedAt finds no unmet past-due record and Fulfilled (its negation) holds. And composition runs through: bothRents is breached because one conjunct (rentUnpaid) is, while eitherRent is fulfilled because one disjunct (rentPaid) is.

Honest caveats (what runs today)

The model declares more of the calculus than the v0.1 executor evaluates, and the source surfaces each residual loudly rather than approximating it silently:

• The universal halves of composition are commented out. “A conjunction is fulfilled when all conjuncts are” and its disjunction dual recurse through a forall/aggregate over the very predicate they define (Fulfilled of a conjunction counts over Fulfilled of its conjuncts). Argon evaluates a genuine restricted forall, but stratified-aggregate semantics require the aggregated predicate in a strictly-lower stratum, so ox build refuses this cycle as OE1317 (recursion through aggregation) rather than evaluating something ill-founded. The supported rephrasing is NAF double-negation (a counter-example helper, then negate it), evaluated under well-founded semantics; adopting it reshapes the rule surface and is deliberate follow-up. The existential halves — conjunction-breached, disjunction-fulfilled — are what evaluate, and the demo exercises exactly those.
• Conditional vesting is declared and admitted but not exercised by the pinned demo. A conditional’s breach depends on its guard being fulfilled, and fulfillment is not breached — a genuine recursion-through-negation cycle, inherent to the deontic logic. The stratifier now flags such SCCs and evaluates them under well-founded semantics (the Van Gelder alternating fixpoint), so the rules pass ox check verbatim; they are left commented only to keep the pinned demo extents stable. The ConditionalPropositionalContent type and its guardOf / consequentOf relations remain in the hierarchy.
• Dates are Int day-numbers. Ordering and interval comparison — all the calculus needs — are exact; day-numbers keep the example runnable because the demo harness cannot yet seed the Date primordial.
• One book per obligation period. A satisfaction account’s records all count toward its period, so Met is the cumulative sum over the account. The intra-account Allen-relation window filter (for accounts spanning many periods) needs multi-condition comprehension where, a documented residual.

This example is compiled and run in CI; its Met / BreachedAt / Fulfilled extents under cumulative aggregation, negation, and existential composition are pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs) to exactly {expPaid} / {rentUnpaid, rentPartial, bothRents} / {rentPaid, eitherRent}. If the language changes underneath it, the build breaks rather than the docs going stale.