vera: Instructions file for Codex

AGENTS.md — Instructions for AI agents

This document is for AI agents working with the Vera codebase. There are two audiences: agents writing Vera code, and agents working on the compiler.

For agents writing Vera code

Read SKILL.md for the full language reference. It covers syntax, slot references, contracts, effects, common mistakes, and working examples that all parse correctly.

Conformance programs as reference

The conformance suite in tests/conformance/ contains small, self-contained programs — named by spec chapter and feature (chNN_feature.vera) — that serve as minimal working examples (most are fully self-contained; the cross-module programs of Chapters 7–9 import companion _lib/module fixtures). Each positive program must pass its declared verification level (see manifest.json for mappings: parse, check, verify, or run); the negative fixtures (the entries with expected_error in tests/conformance/manifest.json) instead must fail with the E-code in their expected_error field, at the stage their expected_error_stage names — check by default, or compile for a diagnostic the checker accepts and codegen refuses. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec.

Workflow

write .vera file -> vera check -> fix errors -> vera verify -> fix errors -> done

Use typed holes (?) to build programs incrementally. A ? in any expression position is valid — vera check reports a W001 warning with the expected type and all available slot bindings:

warning: [W001] Warning at file.vera, line 6, column 3:

      ?
      ^

  Typed hole: expected Int.

  ? is a placeholder for an incomplete expression. The compiler reports the expected type and available bindings so the hole can be filled in.

  Fix:

    Replace ? with an expression of type Int. Available bindings: @Int.0: Int; @Int.1: Int.

  See: Chapter 4, Section 4.17 "Typed Holes"