Prove real programs correct.
Then run them.

An explicit affine dependent type theory. Elixir parses, checks, and emits .muro. Only run terms become running code. Users do not need Agda.

The language book is manual/. That is what muro-lang.dev will render. It is not ExDoc. Elixir API docs, when added, stay on @moduledoc / mix docs. Agda in agda/Muro/ is a third layer: the rules of the calculus, not a certificate that a .muro file is correct.

Install

muro on Hex is published by the murolang organization. Current release: 0.3.0. Releases are listed in CHANGELOG.md.

def deps do
  [
    {:muro, "~> 0.2"}
  ]
end

A clone is for changing the kernel. A .muro file is checked with mix muro.check from a project that depends on the package.

One-shot (humans and agents)

Two jobs. Do not mix them.

You want to…	Do this
Add a Muro program	Write a `.muro` file against `manual/grammar.md`. Check with `mix muro.check path.muro`. Do not change Agda or the Elixir kernel.
Change the type theory	Follow `manual/extending.md`. Agda first, then the matching Elixir clause. Users still only run Mix.

Agents: read manual/for-agents.md. Copy syntax from examples/, not from memory.

Skeleton:

-- comments start with --
def plus : run Π (n : Nat) → Π (m : Nat) → Nat :=
  λ (n : Nat) → λ (m : Nat) →
    match n motive (λ _ → Nat)
      | 0 => m
      | suc np => suc(plus np m)

mix muro.check examples/your_file.muro

A definition is in the book the moment Parser.parse/1 returns it. The checker sees the whole book (forward references are allowed). Emit keeps only run.

Manual

Page	For
Start	Install, first file, emit
The wall	spec / evidence / run
Terms	Π, λ, match, quantities
Grammar	What the parser implements
Examples	Every file in `examples/`
For agents	Operational contract
Limits	What the language does not do

Index: manual/index.md. Machine-readable list: manual/manifest.yml.

Build

mise install
mix deps.get
mix test
mix muro.check
mix muro.check examples/half_ok.muro

Agda 2.8+ and standard library 2.3 (optional unless you change the kernel):

git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git vendor/agda-stdlib
make agda

Muro.Lexer.tokenize/1 is the highlighter. It walks a fragment with the parser's lexical rules and returns {kind, start, stop} byte spans. A snippet that Parser.parse/1 rejects still yields spans, and joining the slices gives the source back. Muro.MakeupLexer maps those spans onto Makeup tags (language "muro", extension .muro) and is registered when the application starts. HTML and colors stay with the caller.

Muro.Check.check_sig/1 returns :ok on the book. CI runs the Elixir job and make agda on every push and pull request. make agda checks the theorem modules (Muro.Judgement, Muro.Typing, Muro.Wall, Muro.Consistency, Muro.Frag, Muro.Tag) under --safe; conversion in ⊢ is a congruent relation generated by a confluent parallel reduction, Muro.Typing proves substitution and preservation for the fragment, Muro.Consistency proves that no closed normal evidence term has type Empty, and Empty-evid itself waits on normalisation of closed evidence. Muro.Soundness proves that the executable checker is sound for ⊢ on the fragment: when Muro.Check accepts a definition over a signature of non-indexed data types, ⊢ derives it with the same uses (one direction only; the module imports Muro.Check, which carries TERMINATING pragmas, so it is checked without --safe). The fragment is Π, λ, application, Nat, Unit, Empty, identity, rewrite, def, annotation, and data: constructor applications and match on a non-indexed data type, with ι for match in the reduction. match on an indexed data type, ν, and Tensor are still outside ⊢. Type is one impredicative sort; kinds (Π (x : A) → Type) are well-formed but are not terms of type Type, in Agda and in Elixir alike.

Names