docs← Back to article

Markdown for LLMs

Definitions: pitfalls

The source Markdown for this article. Copy it into your assistant or download it as a text file.

Download this articlePlain text ↗
# Definitions: pitfalls

> Updated 3 October 2026: `concept`, `except_when`, `claim`, `definition … sufficient`, and `default` strength have been removed, together with their special deprecation diagnostic. References below to the former behavior and corpus sources are historical. New source uses `relation`, `unless`, `duty`, a strict rule, and `defeasible`.

Wrong forms, silent outcomes, `LDC-E` diagnostics, typical mistakes of
formalizers and AI agents, and how to detect them. Items marked
“confirmed by runs” were reproduced during this research on the installed
engine.

## 1. A separate `relation` for the definition name (finding, confirmed by runs)

```law
relation minor(p: Person) kind institutional {
    label ru-KZ official "является несовершеннолетним";
}
definition minor(p: Person) exact {
    when under_eighteen(p);
}
// error LDC-E1201: имя "minor" уже объявлено + LDC-E1338 о двойном StableId
```

A definition and a relation share one namespace: the compiler synthesizes
the relation itself, writing it by hand is a static rejection. The correct
form is a lone definition: `definition Sheaf(f: Presheaf) exact` stands
alone, without any companion `relation`. The AI agent, used to “vocabulary
first, then rules”, writes `relation` automatically — here that is a
mistake. Detection: `LDC-E1201` on a `definition` line means almost always
exactly this, not a random name clash.

## 2. One-way definitions

For a named qualification with both a deriving rule and a necessary
constraint, use `definition … exact`. For a one-way inference, write a
strict `rule` explicitly.

## 3. Expecting contraposition from `exact` (silent outcome)

A `definition` does not apply contraposition: from “of full age”
nothing about age follows until the author writes a separate rule with a
literal head. An explicit negative classification is likewise set by a
separate `rule … then not …`. Detection: a question about the concept’s
negation answers Not established, not refuted on any case — and that is not “facts missing” but
the absence of the reverse direction. A test on the concept’s negation must
exist separately from the test on the concept.

## 4. A definition with exceptions

A definition has no hidden strength: if the qualification has
ordinary exceptions or a presumptive character, take `classification …
defeasible` or separate defeasible rules. A definition “that is almost
always true” is a wrong form choice: the first exception will demand a
rewrite, and until then the definition will give a strict inference where
the law gives a contestable one.

## 5. Redeclaring the definition name

```law
relation minor(p: Person) kind institutional;
definition minor(p: Person) exact { ... }
```

The definition synthesizes its own relation. Declaring the same relation
separately creates a duplicate name and is rejected; use the definition alone.

## 6. A definition without `scope` on a polysemous term

One term can have different definitions in different packages and contexts,
and a legal definition must have scope. Without `scope`, a term
living in two contexts (e.g. “place of residence” in substantive and in
procedural law) gives two unconditional strict inferences under one name — a
hidden definition conflict surfacing as Contradiction at a consumer importing both
packages. Detection: a term with two scopeless definitions is a candidate
for scope refinement; scope is written as a `scope` clause in the
definition body.