n.bend checks

raw source on the hub · import 0xd29b5061c68e1be166e0476f4daf7ff8/n.bend as N

1 import

import Base

Types

type Span source · line 13 · raw

Data

---- source ---- A span of a .n file, by character offsets: [start, end).

Span
```
@start:Nat -> @end:Nat -> Span
```

type Reading source · line 17 · raw

Data

One reading of a span: the Bend term it elaborates to, as text.

Reading
```
@span:Span -> @term:String -> Reading
```

type Stage source · line 22 · raw

Data

---- stages ---- Each question has exactly one owner: N checks the language, then U checks feelings.

N
```
Stage
```
U
```
Stage
```

type Diagnostic source · line 30 · raw

Data

---- type errors ---- Ambiguous: the span has several readings and nothing settles which one is meant. Inconsistent: two readings cannot both hold. Unconfirmed: the author has not confirmed that the reading is what they meant.

Ambiguous

@stage:Stage -> @span:Span -> @readings:List<&2, Reading> -> Diagnostic

Inconsistent

@stage:Stage -> @a:Reading -> @b:Reading -> @why:String -> Diagnostic

Unconfirmed

@stage:Stage -> @reading:Reading -> Diagnostic