Paradigm¶

MLTTDB splits a proof-assistant data workflow into three parts:

Responsibility	Lives in
Table declarations and row types	Proof-assistant source
Ordered records	Term store
Semantic validation	Proof assistant or generated source

The store is deliberately simple. It stores record text and ordering, but it does not parse, elaborate, normalize, or type-check proof-assistant terms.

Tables¶

A table is declared in proof-assistant source with a language-specific table declaration. In Agda, the core form is:

someData :T: RowType

The table identity is its qualified source name, such as:

Demo.Basic.someData

Records stored for that table are validated at the declared row type.

Records¶

Records are stored as ordered UTF-8 source snippets:

{
  "database": "demo",
  "language": "agda",
  "table": "Demo.Basic.someData",
  "records": [
    {
      "uuid": "f3dd124c-b2d0-471b-9c7b-4b4f913567be",
      "body": "myNat zero"
    }
  ]
}

The body field is intentionally opaque to the store. A validator gives it meaning by checking it as proof-assistant source at the table row type.

Modes¶

MLTTDB tools use four modes:

Mode	Use it when
schema	You want to check table declarations without fetching store records.
tables	You want JSON table metadata for creating or updating a database.
data	You want to fetch records and validate them against source tables.
eval	You want a backend to evaluate one expression in the checked context before a selected row.

Native Agda supports these modes directly. Preprocessors provide the same schema, table-discovery, and data workflow by generating ordinary proof-assistant files.

UUIDs And Order¶

Every record has a UUID. Within a database, UUIDs are unique across all tables.

Record order is semantic. Validators process records exactly in store order. In the Agda profile, a record may refer only to records validated earlier in the same run. Preprocessors encode UUIDs into legal generated identifiers where the target proof assistant needs ordinary names.

Databases And Languages¶

Each database has one language:

agda
lean
rocq

Validation requests include the language, and the store rejects requests whose language does not match the database metadata. This prevents accidentally checking Lean records through an Agda path, or the reverse.