For your agent

Point your agent at edda

Edda is written by your coding agent, not learned by you first. Because edda isn't in any model's training data, your agent reads a short setup before it writes a line. This page is that setup — human-readable here, machine-readable at /get-started/agent.txt. You don't change your workflow; your agent adds one file it reads, and optionally some guardrails you approve.

Start with one sentence

Say this to your coding agent. If it can browse the web, it will find this site, read its own setup, scaffold a project, and ask you about the optional guardrails:

I want to use the Edda language — edda-lang.org

Any agent that reads AGENTS.md — Claude Code, Cursor, Codex, Copilot, Gemini, Windsurf, and more — can follow the steps below on its own.

What your agent does

The exact setup your agent follows — served verbatim as plain text at /get-started/agent.txt:

# Edda — agent setup recipe

You are setting up an Edda project for a user, end to end. Edda is a verified
language that is NOT in your training data — do not guess syntax by analogy to
Rust, Swift, Go, or OCaml; it will not compile. Work these steps in order. The
end state is a small, built, contract-verified project the user can keep as a
reusable starter template.

## 1. Read the reference (before writing any Edda)
Fetch https://edda-lang.org/AGENTS.md and load it in full — the canonical,
always-on language reference. Fetch https://edda-lang.org/guide.md on demand for
special operations (verification tooling, property testing, capability
typestate, distribution). Do not write a line of Edda until AGENTS.md is in
context.

## 2. Install the toolchain
The prebuilt installer bundles the `edda` binary, its runtime, and a vendored
`std` + `runes` — nothing else to fetch, no environment variable to set. Pick
your host:
  - Windows (PowerShell), the verified platform:
      irm https://raw.githubusercontent.com/edda-lang/edda-bootstrap/main/install.ps1 | iex
  - Linux / macOS (archives still rolling out; if there is no release asset for
    your platform yet the installer says so — fall back to a source build per
    the edda-bootstrap README):
      curl -fsSL https://raw.githubusercontent.com/edda-lang/edda-bootstrap/main/install.sh | bash
The installer adds `edda` to PATH, but your CURRENT shell won't see it yet.
Start a new shell, or call the full path for the first check:
      edda version                        (new shell)
      ~/.edda-bootstrap/bin/edda version  (same shell; edda.exe on Windows)
Expect `edda (bootstrap-rust) <version>` and your host target.

## 3. Set up YOUR harness (its native config, not just a dropped file)
Identify which coding agent you are, then create that harness's native project
config so the reference auto-loads every session. Place AGENTS.md at the repo
root in every case — the cross-tool standard 30+ agents read — then add the
harness-native piece:
  - Claude Code:    CLAUDE.md whose first line is  @AGENTS.md  (plus a .claude/ dir).
  - Cursor:         AGENTS.md at root (read directly).
  - OpenAI Codex:   AGENTS.md at root.
  - GitHub Copilot: .github/copilot-instructions.md that points at AGENTS.md.
  - Gemini CLI:     AGENTS.md at root (GEMINI.md also read if present).
  - Windsurf:       .windsurfrules that points at AGENTS.md.
  - Unknown harness: place AGENTS.md at root and create whatever project-memory
    file your harness auto-loads, pointing it at AGENTS.md. Degrade gracefully —
    if there is no such concept, AGENTS.md at root is enough.

## 4. Install the Edda skill (the special-operations tier)
Fetch https://edda-lang.org/skill.md — a short, agent-agnostic skill that points
you at the authoring guide and the compiling examples for anything past everyday
syntax. Render it in your harness's native skill format:
  - Claude Code:   write it to  .claude/skills/edda-authoring/SKILL.md
  - Other harness: save it where your harness discovers skills, or keep it as a
    project doc and read it when a task needs special operations.
Everyday syntax stays in AGENTS.md; the skill is the deeper tier on top.

## 5. Reading-discipline hooks — ASK the user first; never install silently
Edda can enforce a reading discipline mechanically: before editing a .ea file
you first read the compiler-emitted index.toon structure maps down its directory
chain, and oversized reads are capped to a bounded span. Two scripts do it —
toon_gate.py (the gate) and toon_ledger.py (records which maps you have read).

Be honest when you ask: these are currently Claude-Code-shaped (PreToolUse /
PostToolUse hooks that emit JSON deny decisions) and need Python on PATH. They
earn their keep on large, multi-directory codebases and are nearly inert on a
small starter. Offer them only if your harness supports equivalent pre-tool
hooks. Present this and WAIT for a yes / no:

  Optional: I can install two hook scripts that make me read Edda's structure
  maps before editing source and stop me from reading whole oversized files at
  once. Upside: I stay grounded and spend fewer tokens on big codebases. Cost:
  an extra read step per edit, Python on PATH, and a one-time settings change.
  Install them? (yes / no)

If yes: fetch https://edda-lang.org/hooks/toon_gate.py and
https://edda-lang.org/hooks/toon_ledger.py, wire toon_gate to your pre-tool hook
and toon_ledger to your post-tool hook (treat a non-zero gate decision as deny),
and set EDDA_TOON_SUBTREES to your own source directory (e.g. `src`) — the
default targets a monorepo, not a single-package project. If no: skip; nothing
else changes.

## 6. Scaffold a small, real project
Create a package that builds clean and teaches the contract loop — one
capability, one requires/ensures. This matches https://edda-lang.org/get-started.

  package.toml:
    [package]
    name = "hello"
    version = "0.1.0"
    root_namespace = "hello"

    [build]
    default_target = "x86-64-windows-msvc"

  Set default_target to YOUR host triple in dash form (x86-64-linux-gnu,
  aarch64-macos-darwin, ...). `edda version` prints the same triple with
  underscores (x86_64-windows-msvc); it is the same target — package.toml uses
  the dash form.

  src/main.ea:
    module hello.main

    import std.io.stream

    function non_negative(x: i64) -> i64
        requires x >= 0
        ensures result >= 0
    {
        return x
    }

    public function main(out: Stdout) -> ()
        with {out}
    {
        let y = non_negative(7)
        out.print_line(f"non_negative(7) = {y}")
    }

Work from a neutral directory — NOT a sibling of a local edda-stdlibs or edda
monolith checkout, or the compiler may adopt that sibling as the active std and
shadow the bundled one.

## 7. Build, run, and prove verification is real
From the project directory:
      edda check     fast type-only loop
      edda build     typecheck + discharge every contract + emit a binary
      edda run       build, then execute (prints: non_negative(7) = 7)
Now delete the `requires x >= 0` line and run `edda build` again. The compiler
refuses and hands back a concrete counter-example (x = -1) instead of compiling
a bug. Put the line back; the build is green. That refusal is the point of
Edda — the build is the source of truth.

## 8. Leave a reusable template
Tell the user in plain words: this directory is a clean, contract-verified Edda
starter they can copy for any future project, or re-run this recipe to
regenerate. (A `git clone` starter, edda-lang/edda-starter, is planned as a
shortcut.) You are done when `edda build` is green.

Machine-readable entry points