docs← Back to article

Markdown for LLMs

LDC-E1308 — Noncanonical defeater spelling

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

Download this articlePlain text ↗
# LDC-E1308 — Noncanonical defeater spelling

## What it means

This warning family has two cases: a `defeat` clause with a strength other
than `defeater` (the strength is corrected), and `defeater` with a `then`
head (the head attacks the written polarity). The message distinguishes
them. `default` is not a supported rule strength and is refused with E0201;
it is not a third interpretation of this warning.

A defeater attacks an inference; it does not derive one. Its head
names the attacked conclusion, and the canonical spelling is the
`defeat` clause — a `then` part on a defeater reads "derive" while
executing "block", with polarity taken literally. The compiler keeps
the node but warns at the strength, so the author can move the head
into the canonical shape.

The repair is to spell the attack: replace the `then` part with
`defeat` over the attacked atom. Note the polarity trap the message
names — `then not X` attacks candidates for `not X`, not for `X`.

## Example

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

relation p(x: Text) kind institutional;
relation q(x: Text) kind institutional;
rule X1 defeater {
    for v0: Text;
    when p(v0);
    then q(v0);
}
```

## Fix

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

relation p(x: Text) kind institutional;
relation q(x: Text) kind institutional;
rule Base defeasible {
    for v0: Text;
    when p(v0);
    then q(v0);
}
rule X1 defeater {
    for v0: Text;
    when p(v0);
    defeat q(v0);
}
```

## Engine message

The engine reports this in its own wording:

```text
example.law:7:9: warning LDC-E1308: rule "X1": defeater strength with a `then` part (§95.3); the defeater head names the ATTACKED inference, not the derived one — the canonical form is `defeat <atom>`. `then not X` attacks candidates for `not X`, not for `X`
```

## Related

- [Defeasible rules and unless](/constructs/rule-defeasible-unless/) — defeaters and the attacks they spell.
- [Priority](/constructs/priority/) — ordering the inferences that survive attack.