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.
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.
the VALUE side of the value/ontology boundary — struct and enum as language built-ins (§5.1). 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.”
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
the negative-enforcement half of the test atom (§17.14). 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.
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 fulfilledas of a date. The capstone of the corpus.