Markdown for LLMs

import-ir

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

# import-ir

Reference page for the `import-ir.schema.json` JSON schema.

## Versions

Accepted `format`: `arxo.import/0.1`.

## Top-level fields

| name | type-or-$ref | required | description |
|---|---|---|---|
| `format` | `"arxo.import/0.1"` | yes | — |
| `snapshot` | [`#/$defs/Snapshot`](#snapshot) | yes | — |
| `documents` | `object` | yes | — |
| `anchors` | `object` | yes | — |
| `modules` | `object` | yes | — |
| `symbols` | `object` | yes | — |
| `expressions` | `object` | yes | — |
| `declarations` | `object` | yes | — |
| `dependencies` | `array` | yes | — |
| `facts` | `object` | no | — |
| `dependency_completeness` | enum (2) | no | — |

## Enumerations

| location | values |
|---|---|
| `properties/format` | `"arxo.import/0.1"` |
| `properties/dependencies/items/properties/kind` | `"type"`, `"statement"`, `"definition"` |
| `properties/facts/additionalProperties/properties/args/items/oneOf/0/properties/kind` | `"entity"` |
| `properties/facts/additionalProperties/properties/args/items/oneOf/1/properties/kind` | `"string"` |
| `properties/dependency_completeness` | `"module"`, `"declaration"` |
| `$defs/Symbol/properties/kind` | `"type"`, `"predicate"` |
| `$defs/Expression/oneOf/0/properties/kind` | `"var"` |
| `$defs/Expression/oneOf/1/properties/kind` | `"atom"` |
| `$defs/Expression/oneOf/2/properties/kind` | `"and"` |
| `$defs/Expression/oneOf/3/properties/kind` | `"or"` |
| `$defs/Expression/oneOf/4/properties/kind` | `"implies"` |
| `$defs/Expression/oneOf/5/properties/kind` | `"forall"` |
| `$defs/Expression/oneOf/6/properties/kind` | `"exists"` |
| `$defs/Expression/oneOf/7/properties/kind` | `"not"` |
| `$defs/Expression/oneOf/8/properties/kind` | `"equal"` |
| `$defs/Expression/oneOf/9/properties/kind` | `"opaque"` |
| `$defs/Declaration/properties/kind` | `"theorem"`, `"definition"`, `"axiom"`, `"instance"` |

## Raw schema

[`https://law.arxo.io/schema/import-ir.schema.json`](https://law.arxo.io/schema/import-ir.schema.json)

## `Snapshot`

Type: `object`.
Required: `project`, `revision`, `language`, `logic`, `adapter`, `context_complete`, `retrieved_at`, `requires`.

| name | type-or-$ref | description |
|---|---|---|
| `project` | `string` | — |
| `revision` | `string` | — |
| `language` | `string` | — |
| `logic` | `string` | — |
| `adapter` | `string` | — |
| `context_complete` | `boolean` | — |
| `retrieved_at` | `string` | — |
| `requires` | `array` | — |

## `Document`

Type: `object`.
Required: `uri`, `language`, `official`, `text`, `content_hash`.

| name | type-or-$ref | description |
|---|---|---|
| `uri` | `string` | — |
| `language` | `string` | — |
| `official` | `boolean` | — |
| `text` | `string` | — |
| `content_hash` | `string` | — |

## `Anchor`

Type: `object`.
Required: `document`, `start`, `end`, `locator`.

| name | type-or-$ref | description |
|---|---|---|
| `document` | `string` | — |
| `start` | `integer` | — |
| `end` | `integer` | — |
| `locator` | `string` | — |

## `Symbol`

Type: `object`.
Required: `kind`, `parameters`, `label`.

| name | type-or-$ref | description |
|---|---|---|
| `kind` | enum (2) | — |
| `parameters` | `array` | — |
| `label` | `string` | — |

## `Expression`

Definition `Expression`.

## `Declaration`

Type: `object`.
Required: `module`, `kind`, `label`, `parameters`, `context`, `statement`, `anchor`, `requires`.

| name | type-or-$ref | description |
|---|---|---|
| `module` | `string` | — |
| `kind` | enum (4) | — |
| `label` | `string` | — |
| `parameters` | `array` | — |
| `context` | `array` | — |
| `statement` | `string` | — |
| `anchor` | `string` | — |
| `requires` | `array` | — |