Skip to main content

Grammar — EBNF

This page is the authoritative specification of Verum's concrete syntax. The full EBNF runs to a little under twenty-five hundred lines (version 3.0); every parser, IDE integration, and proof tool in the project must conform to it.

Status

Version 3.0 — Production-Ready · Formal Specification. All parsers, IDE tooling, and proof tooling must conform to this grammar.

Reading conventions​

The grammar uses ISO-style EBNF with these meta-symbols:

NotationMeaning
=rule definition
,concatenation
|alternation
[...]optional (zero or one)
{...}repetition (zero or more)
(...)grouping
'literal' or "literal"terminal symbol
..character range (e.g., 'a'..'z')
(* ... *)comment in source
epsilonempty production

Rule names are snake_case. Terminals are quoted.

Design principles encoded in the grammar​

Every production reflects a deliberate language decision. Six pervade:

  1. Reserved keywords are exactly three — let, fn, is. Everything else is contextual.
  2. Unified type definitions — type T is … covers records, variants, protocols, sigma types, aliases, and existentials.
  3. Explicit context system — using [...] is mandatory for effects.
  4. Three-tier references — &T, &checked T, &unsafe T.
  5. No !-suffix macros — every compile-time construct uses @.
  6. is operator replaces matches!() — patterns are first-class in expressions.

Layer 1 — Lexical Grammar​

1.1 Whitespace and comments​

whitespace      = ' ' | '\t' | '\r' | '\n' ;
line_comment    = '//' , { char_except_newline } , '\n' ;
block_comment   = '/*' , { char_except_star_slash } , '*/' ;
comment         = line_comment | block_comment ;

Block comments do not nest (intentional — keeps lexer trivial). Doc comments are surface sugar (/// → @doc("…")).

1.2 Identifiers​

ident_start     = letter | '_' ;
ident_continue  = letter | digit | '_' ;
identifier      = ident_start , { ident_continue } ;
type_param_name = uppercase_letter , { ident_continue } ;

letter and digit admit Unicode (unicode_letter, unicode_digit) in addition to ASCII — Verum source is fully Unicode-clean. Type parameter names are conventionally upper-camel.

1.3 Keywords​

Reserved (3)​

reserved_keyword = 'let' | 'fn' | 'is' ;

These are never identifiers under any circumstance.

Contextual (~60)​

Grouped as in the EBNF source:

GroupKeywords
Primarytype, where, using
Control flowif, else, match, return, for, while, loop, break, continue
Async / concurrencyasync, await, spawn, defer, errdefer, try, yield, throws, select, nursery
Modifierspub, mut, const, unsafe, pure
FFIffi
Module systemmodule, mount, implement, context, protocol, extends
Misc.self, super, crate, static, meta, provide, finally, recover, invariant, decreases, stream, tensor, affine, linear, public, internal, protected, ensures, requires, result, some
Proof DSLtheorem, lemma, axiom, corollary, proof, calc, have, show, suffices, obtain, by, qed, induction, cases, contradiction, forall, exists
AST-alignmentref, move, as, in, Self, private, checked, view, extern, cofix, dyn, biased

default is not in the grammar's keyword list — it is handled as a contextual identifier in impl_item so that fn default() and T.default() continue to parse.

1.4 Literals​

1.4.1 Numeric​

decimal_lit     = dec_digit , { dec_digit | '_' } ;
hexadecimal_lit = '0x' , hex_digit , { hex_digit | '_' } ;
octal_lit       = '0o' , oct_digit , { oct_digit | '_' } ;
binary_lit      = '0b' , bin_digit , { bin_digit | '_' } ;

int_suffix      = 'i8' | 'i16' | 'i32' | 'i64' | 'i128' | 'isize'
                | 'u8' | 'u16' | 'u32' | 'u64' | 'u128' | 'usize' ;
float_suffix    = 'f32' | 'f64' ;

integer_lit     = ( decimal_lit | hexadecimal_lit | octal_lit | binary_lit )
                , [ int_suffix ] ;
float_lit       = decimal_lit , '.' , decimal_lit , [ exponent ] , [ float_suffix ] ;
exponent        = ( 'e' | 'E' ) , [ '+' | '-' ] , decimal_lit ;

Underscores allowed anywhere inside the digits (1_000_000); no underscore required before a suffix (42i32).

1.4.2 Text​

Verum has two text literal forms (intentionally minimal):

plain_string    = '"' , { string_char | escape_seq } , '"' ;
raw_multiline   = '"""' , { any_char - '"""' | '""""' } , '"""' ;
string_lit      = plain_string | raw_multiline ;
byte_string_lit = 'b' , '"' , { byte_string_char | byte_escape_seq } , '"' ;
char_lit        = "'" , ( char | escape_seq ) , "'" ;

Triple-quote = always raw, multiline-capable. To embed """ literally, use four quotes ("""" ... """"). The Rust-style r#"…"# is deliberately removed.

escape_seq = '\' , ( 'n' | 'r' | 't' | '0' | 'a' | 'b' | 'f' | 'v'
                  | '\' | '"' | "'"
                  | 'x' , hex_digit , hex_digit
                  | 'u' , '{' , hex_sequence , '}' ) ;

1.4.3 Format strings (interpolation)​

interpolated_string = ( 'f' | 'fmt' ) , '"' , { string_char | interpolation } , '"' ;
interpolation       = '{' , expression , [ ':' , format_spec ] , '}' ;

Embedding arbitrary expressions: f"x = {x}, y = {y + 1:.3}".

1.4.4 Tagged literals​

tagged_literal      = format_tag , '#' , tagged_content ;
tagged_content      = plain_string | raw_multiline ;

tagged_interpolated = format_tag , '#' , tagged_interpolated_content ;
tagged_interpolation = '${' , expression , '}' ;

The format tag enables compile-time content validation by category:

CategoryTags
Data interchangejson, json5, yaml, toml, xml, html, csv
Query languagessql, gql, graphql, cypher, sparql
Pattern matchingrx, re, regex, glob, xpath, jpath
Identifiersurl, uri, email, path, mime, uuid, urn
Temporald, dur, tz, date, time, datetime
Networkingip, cidr, mac, host
Versioning / encodingver, semver, b64, hex, pct
Structuredmat, vec, interval, ratio, tensor
Code / DSLsh, css, lua, asm, contract
Scientificchem, music, geo
Customany identifier

json#"…", sql#"""…""", rx#"…", url#"…" — the parser dispatches to the tag's validator and constructs the corresponding semantic type (JsonValue, SqlQuery, Regex, Url, …) at compile time. Invalid content is a compile error, not a runtime exception.

1.4.5 Composite & context-adaptive literals​

composite_literal = identifier , '#' , composite_body ;
composite_body    = composite_string | composite_paren | composite_bracket | composite_brace ;
                    (* identifier#"…" | #( … ) | #[ … ] | #{ … } *)

context_adaptive_lit = bare_token ;
bare_token       = identifier | hex_color_literal | at_literal | dollar_literal ;
hex_color_literal = '#' , hex_digit{6} , [ hex_digit{2} ] ;   (* #RRGGBB or #RRGGBBAA *)
at_literal       = '@' , identifier ;                          (* @tag *)
dollar_literal   = '$' , identifier ;                          (* $name *)

1.4.6 Boolean​

bool_lit = 'true' | 'false' ;

1.5 Operators​

arith_op       = '+' | '-' | '*' | '/' | '%' | '**' ;
compare_op     = '==' | '!=' | '<' | '>' | '<=' | '>=' ;
logical_op     = '&&' | '||' | '!' ;
bitwise_op     = '&' | '|' | '^' | '<<' | '>>' | '~' ;
assign_op      = '=' | '+=' | '-=' | '*=' | '/=' | '%='
               | '&=' | '|=' | '^=' | '<<=' | '>>=' ;
range_op       = '..' | '..=' ;
pipe_op        = '|>' ;
arrow_op       = '->' | '=>' ;
optional_chain = '?.' ;
null_coalesce  = '??' ;

For full precedence, see Operators.

1.6 Punctuation​

punctuation = '(' | ')' | '[' | ']' | '{' | '}'
            | '<' | '>' | ',' | ';' | ':' | '.' | '@'
            | '?' | '&' | '|' | '%' | '!' | '#' | '_' ;

Layer 2 — Syntactic Grammar​

2.1 Programs and items​

program      = { program_item } ;
program_item = item | statement ;

item = function_def
     | type_def
     | impl_block
     | extern_block
     | context_def
     | context_protocol_def
     | context_type_protocol_def
     | context_group_def
     | const_def
     | static_def
     | mount_stmt
     | module_def
     | meta_def
     | pattern_def
     | ffi_declaration
     | attribute_item ;

2.2 Visibility and attributes​

visibility = 'public' | 'internal' | 'protected' | epsilon ;

attribute_item = '@' , attribute , item ;
attribute      = std_attribute
               | specialize_attribute
               | derive_attribute
               | verify_attribute
               | identifier , [ '(' , attribute_args , ')' ] ;
attribute_args = expression_list | named_arg_list ;
named_arg_list = named_arg , { ',' , named_arg } ;
named_arg      = identifier , '=' , expression ;

std_attribute        = 'std' , [ '(' , identifier , ')' ] ;
specialize_attribute = 'specialize' ;
derive_attribute     = 'derive' , '(' , identifier , { ',' , identifier } , ')' ;

verify_attribute = 'verify' , '(' , verify_strategy_list , ')' ;
verify_strategy_list = verify_strategy
                     | '[' , verify_strategy , { ',' , verify_strategy } , ']' ;
verify_strategy = 'runtime' | 'static' | 'fast'
                | 'complexity_typed'
                | 'formal' | 'proof'
                | 'thorough' | 'reliable' | 'certified'
                | 'coherent_static' | 'coherent_runtime' | 'coherent'
                | 'synthesize'
                | 'assume' ;

@verify selects a semantic strategy rather than a particular solver — the compiler chooses an adapter or portfolio per the router. See SMT routing.

The fourteen accepted strategies are arranged on a strictly monotone ν-ordinal ladder (see Gradual verification for the full ladder). The list-form chains a fallback sequence: @verify([proof, static, runtime]) runs proof first; on failure falls back to static, then runtime. Chains are written left-to-most-trusted; the kernel rejects monotonicity-violating chains like @verify([runtime, proof]). assume is the off-ladder escape hatch — using it in a chain disables verification for the remainder of the chain and is audit-tracked via verum audit --assumptions.

Attribute classification (the architecture rework)​

Verum's attributes split into two architectural classes:

1. Compiler-internal typed attributes — recognised by name in the parser; their semantic shape lives in verum_ast::attr::typed::* because Rust passes (TCB / pipeline / audit walker / CLI driver) dispatch on them at compile time:

AttributeSpecDispatch site
@verify(strategy)§12verum_smt::verify_strategy::extract_from_attributes
@framework(name, "cite")§6verum_kernel::axiom::load_framework_axioms (TCB)
@framework_translate(s, t, "cite")Task C7bverum_cli::audit::collect_framework_markers_from
@extract[(target)] / @extract_witness[(target)] / @extract_contract[(target)]§8.6verum_cli::extract::collect_extract_requests
@enact(epsilon = "...")§11verum_cli::audit::audit_epsilon
@accessibility(λ)Diakrisis Axi-4audit walker
@quantity(0 | 1 | omega)§7.6type checker
@derive(Trait, ...)§8.7derive macros
@cfg(...)§3.2conditional compilation
@inline / @cold / @repr(C) / etc.misccode generation hints
@arch_module(...)ATS-Vverum_kernel::arch + ATS-V phase 6.5

2. Meta-system advisory attributes — parsed via the generic identifier(args) form; semantic validation happens in core/meta/diakrisis_attrs.vr (and other meta-modules). No parser extension required; users may define analogous classifiers in their own meta-modules:

AttributeSpecMeta-fn
@effect(kind)Part B §9parse_effect_attr
@infinity_category(level)Part B §4parse_infinity_category
@autopoietic(epsilon, depth)Part B §5parse_autopoietic
@ludic_designPart B §10parse_ludic_design
@cut_elimination[(bound)]Part B §10parse_cut_elimination

Architectural principle (V8.1 META1): typed attributes are reserved for compiler-internal dispatch where performance or TCB constraints matter. Every advisory marker that does NOT participate in compile-time dispatch is BETTER expressed via the meta-system — zero grammar bloat, user-extensible, single source of truth (definition + validation + docstring + spec citation all in one .vr file).

ATS-V @arch_module(...) — ATS-V Architectural Type System​

The @arch_module(...) typed attribute (per ATS-V spec §8) takes named arguments parsed via the generic attribute_args = named_arg_list form (no new grammar production). Every field reuses canonical Verum syntax: variant constructors for enum-typed fields, list literals for collections, identifier paths for references.

@arch_module(
    exposes = [Capability::Authenticate, Capability::IssueToken],
    requires = [Capability::HashPassword, Capability::RandomBytes],
    preserves = [SessionInvariant::NoTokenLeak],
    at_tier = Tier::MultiTier([Tier::Aot, Tier::Interp]),
    foundation = Foundation::ZfcTwoInacc,
    stratum = MsfsStratum::LFnd,
    lifecycle = Lifecycle::Theorem("v0.1"),
    cve_closure_C = synthesize_session_token,    // C — Constructive
    cve_closure_V_strategy = certified,          // V — @verify ladder
    cve_closure_E = AuthenticationServer,        // E — Executable entry point
    composes_with = [Database::transactional, Network::tls_v13],
    strict = true,
)
public module authentication { ... }

The ATS-V phase (the architectural-type-checking phase in the compiler pipeline) parses @arch_module(...) named-args into a canonical Shape record (mirror of the kernel-side Shape type), runs anti-pattern checks across the 40-pattern catalog (AP-001..AP-040), and emits structured diagnostics with stable RFC error codes under a dual-audience design (machine-readable

  • human-readable in the same surface).

See Architecture-as-Types for the full architectural type system surface and anti-pattern catalog for the 40-pattern reference.

2.3 Modules and imports​

mount_stmt   = 'mount' , mount_tree , [ 'as' , identifier ] , ';' ;
mount_tree   = mount_item , [ 'as' , identifier ]
             | path , '.' , '{' , mount_list , '}'
             | path , '.' , '*' ;
mount_list   = mount_tree , { ',' , mount_tree } ;

module_def   = visibility , 'module' , module_path , module_body ;
module_path  = identifier , { '.' , identifier } ;
module_body  = '{' , { program_item } , '}' | ';' ;

path         = [ '.' ] , path_segment , { '.' , path_segment } ;
path_segment = identifier | 'self' | 'super' | 'crate' ;

2.4 Type definitions — unified is syntax​

linearity_qualifier = 'linear' | 'affine' ;

type_def = visibility , 'type' , [ linearity_qualifier ] , identifier , [ generics ]
         , [ meta_where_clause ]
         , 'is' , type_definition_body ;

type_definition_body =
      type_expr , [ type_refinement ] , ';'      (* alias / refinement *)
    | sigma_bindings , ';'                       (* dependent pair *)
    | '(' , type_list , ')' , ';'                (* newtype / tuple *)
    | '{' , field_list , '}' , [ type_refinement ] , ';'  (* record *)
    | variant_list , ';'                         (* sum type *)
    | protocol_def , ';' ;                       (* protocol *)

Records​

field_list = [ field , { ',' , field } , [ ',' ] ] ;
field      = { attribute } , [ visibility ] , identifier , ':' , type_expr , [ field_default ] ;
field_default = '=' , expression ;

(* Record types (as type expressions) accept an optional trailing
   row extension for row polymorphism (T1-E). A closed record omits
   the extension; an extensible record captures additional fields in
   the row variable. See language/row-polymorphism.md for semantics,
   the `lacks` predicate, and splat syntax. *)
record_type   = '{' , [ field_list ] , [ row_extension ] , '}' ;
row_extension = '|' , row_expr ;
row_expr      = identifier                                 (* single row var *)
              | identifier , { ',' , identifier } ;        (* row split *)

{ x: Int } is closed; { x: Int | r } is open with r capturing the remaining fields. A lacks-constraint r # x (inferred or written where r # x) ensures r does not already contain x.

Variants (sum types)​

variant_list    = [ '|' ] , variant , { '|' , variant } ;
variant         = { attribute } ,
                  variant_name ,               (* any keyword is allowed *)
                  [ variant_data ] ,
                  ( path_endpoints | path_annotation )? ;
variant_data    = '{' , field_list , '}' | '(' , type_list , ')' ;
path_endpoints  = '=' , expression , '..' , expression ;          (* range form *)
path_annotation = ':' , type_expr ;                               (* type-annotation form *)

A variant that ends in = a..b or : Path<C>(a, b) is a higher-inductive type path constructor (cubical HoTT). Both forms lower to the same path_endpoints metadata; choose whichever is idiomatic for your domain:

// Range form — concise.
type S1_range is Base | Loop() = Base..Base;
type Interval is Zero | One   | Seg()  = Zero..One;

// Type-annotation form — mirrors `Path<C>(a, b)` surface syntax used
// throughout `core/math/hott.vr`.
type S1 is
    | base
    | loop: Path<S1>(base, base);

type Susp<A> is
    | north
    | south
    | merid(a: A): Path<Susp<A>>(north, south);

type Pushout<A, B, C>(f: fn(C) -> A, g: fn(C) -> B) is
    | inl(a: A)
    | inr(b: B)
    | push(c: C): Path<Pushout<A, B, C>(f, g)>(inl(f(c)), inr(g(c)));

Variant names live in their own namespace (Type.Variant), so reserved keywords such as loop, merid, trunc_path, or push are valid constructor identifiers.

Sigma (dependent pair) types​

sigma_bindings = sigma_binding , { ',' , sigma_binding } ;
sigma_binding  = identifier , ':' , type_expr , [ 'where' , expression ] ;
type SizedVec is n: Int, data: [Int; n];
type Matrix   is rows: Int, cols: Int, data: [[Float; cols]; rows];

Protocols​

protocol_def       = 'protocol' , protocol_body ;
protocol_body      = [ protocol_extension ] , [ generic_where_clause ] , '{' , protocol_items , '}' ;
protocol_extension = 'extends' , trait_path , { '+' , trait_path } ;

Refinements​

type_refinement = inline_refinement | value_where_clause ;
inline_refinement = '{' , refinement_predicates , '}' ;
refinement_predicates = refinement_predicate , { ',' , refinement_predicate } ;
value_where_clause = 'where' , [ 'value' ] , refinement_expr ;
type Probability is Float { 0.0 <= self && self <= 1.0 };
type SortedList<T: Ord> is List<T> where self.is_sorted();

2.5 Functions​

function_def = visibility , function_modifiers , fn_keyword , identifier
             , [ generics ] , '(' , param_list , ')'
             , [ throws_clause ]
             , [ '->' , type_expr , [ ensures_clause ] ]
             , [ context_clause ]
             , [ generic_where_clause ]
             , [ meta_where_clause ]
             , function_body ;

fn_keyword          = 'fn' , [ '*' ] ;             (* fn* = generator *)
function_modifiers  = [ 'pure' ] , [ meta_modifier ] , [ 'async' ] , [ 'cofix' ] , [ 'unsafe' ] | epsilon ;
meta_modifier       = 'meta' , [ '(' , stage_level , ')' ] ;
stage_level         = integer_lit ;

throws_clause       = 'throws' , '(' , error_type_list , ')' ;
error_type_list     = type_expr , { '|' , type_expr } ;

ensures_clause      = 'where' , ensures_item , { ',' , ensures_item } ;
ensures_item        = 'ensures' , expression ;

function_body       = copattern_body | block_expr | '=' , expression , ';' | ';' ;
copattern_body      = '{' , copattern_arm , { ',' , copattern_arm } , [ ',' ] , '}' ;
copattern_arm       = '.' , identifier , '=>' , expression ;

Modifier order is fixed and enforced by the grammar: pure → meta(N) → async → cofix → unsafe.

ModifierEffect
purecompiler-verified no side effects
meta, meta(N)compile-time execution; staged at level N
asyncreturns Future<T>
cofixcoinductive fixpoint; body must be copattern_body
unsafebypasses safety guarantees

Parameters​

param_list      = [ param , { ',' , param } , [ ',' ] ] ;
param           = param_pattern | self_param ;
param_pattern   = { attribute } , pattern , ':' , type_expr ;
self_param      = { attribute } , [ ref_modifier ] , 'self' ;
ref_modifier    = '&' , [ ref_kind ] , [ 'mut' ] ;
ref_kind        = 'checked' | 'unsafe' | epsilon ;

2.6 Generics​

generics       = '<' , generic_params , '>' ;
generic_params = generic_param , { ',' , generic_param } ;
generic_param  = extended_generic_param ;

extended_generic_param =
      kind_annotated_param
    | extended_type_param
    | hk_type_param
    | meta_param
    | context_param
    | universe_param
    | level_param ;

extended_type_param  = identifier , [ hk_params ] , [ ':' , bounds ] ;
hk_params            = '<' , '_' , { ',' , '_' } , '>' ;       (* placeholder HKT *)

kind_annotated_param = identifier , ':' , kind_expr , [ '+' , bounds ] ;
kind_expr            = 'Type' , [ '->' , kind_expr ]
                     | '(' , kind_expr , ')' ;

context_param        = 'using' , identifier ;                  (* context polymorphism *)
universe_param       = 'universe' , identifier ;
level_param          = identifier , ':' , 'Level' ;
meta_param           = identifier , ':' , 'meta' , type_expr , [ refinement ] ;

bounds         = bound , { '+' , bound } ;
bound          = protocol_bound | associated_type_bound | negative_bound ;
negative_bound = '!' , protocol_path ;

Type-level features​

type_function_def      = 'type' , identifier , '<' , type_function_params , '>' , '=' , type_expr , ';' ;
constrained_type_alias = 'type' , identifier , '<' , constrained_params , '>'
                       , '=' , type_expr , [ type_alias_where ] , ';' ;

existential_type       = 'some' , identifier , ':' , existential_bounds ;
existential_bounds     = existential_bound , { '+' , existential_bound } ;

(* 2.4.7: type-level literals and meta-arithmetic in type position *)
type_level_literal     = integer_lit | bool_lit | char_lit ;
extended_type_arg      = type_expr | expression | type_level_literal | meta_type_expr ;

2.7 Types​

type_expr  = simple_type , [ type_refinement ] ;

simple_type = primitive_type
            | never_type             (* ! *)
            | unknown_type           (* unknown *)
            | path_type_expr         (* Path<A>(a, b) — cubical *)
            | path_type
            | tuple_type
            | record_type
            | array_type             (* [T; N] *)
            | slice_type             (* [T] *)
            | managed_reference_type (* &T, &mut T *)
            | checked_reference_type (* &checked T *)
            | unsafe_reference_type  (* &unsafe T *)
            | pointer_type           (* *const, *mut, *volatile *)
            | function_type
            | rank2_function_type
            | pi_type                (* Pi (x: A) . B — explicit dependent fn *)
            | tensor_type_expr       (* tensor<...> T — shape-typed array *)
            | universe_type          (* Type, Type(n), Prop *)
            | generic_type
            | genref_type            (* GenRef<T> *)
            | higher_kinded_type     (* F<_> *)
            | existential_type       (* some T: P *)
            | inferred_type          (* _ *)
            | dynamic_type           (* dyn P + Q *)
            | capability_type ;      (* T with [...] *)

primitive_type = 'Int' | 'Float' | 'Bool' | 'Char' | 'Text' | '()' | 'Interval' | 'Prop' ;
never_type     = '!' ;
unknown_type   = 'unknown' ;

References (three tiers)​

managed_reference_type  = '&' , [ 'mut' ] , type_expr ;            (* CBGR-checked *)
checked_reference_type  = '&' , 'checked' , [ 'mut' ] , type_expr ; (* zero-cost, proven *)
unsafe_reference_type   = '&' , 'unsafe' , [ 'mut' ] , type_expr ;  (* zero-cost, asserted *)

pointer_type = '*' , ( 'const' | 'mut' | 'volatile' , [ 'mut' ] ) , type_expr ;

Function types​

function_type       = [ 'async' ] , 'fn' , '(' , type_list , ')' ,
                      [ '->' , type_expr ] , [ context_clause ] ;

(* Rank-2: function type quantifies its own type parameters *)
rank2_function_type = [ 'async' ] , 'fn' , generics , '(' , type_list , ')' ,
                      [ '->' , type_expr ] , [ context_clause ] , [ generic_where_clause ] ;

Dependent function types (Π)​

pi_type   = 'Pi' , pi_binder , { pi_binder } , '.' , type_expr ;
pi_binder = '(' , identifier , ':' , type_expr , [ 'where' , expression ] , ')'
          | '{' , identifier , ':' , type_expr , [ 'where' , expression ] , '}' ;

Round brackets denote explicit parameters; curly braces denote implicit parameters (synthesised by inference, like Agda/Lean).

type ReplicateOf<T>  is Pi (n: Int) . [T; n];
type At<T>           is Pi {n: Int} (i: Int where i < n) . T;

All three surface forms — value-dependent fn, where/ensures, and explicit Pi — elaborate to the same Ty::Pi node. See dependent types.

Universe hierarchy​

universe_type       = 'Type' , [ '(' , universe_level_expr , ')' ]
                    | 'Prop' ;

universe_level_expr = universe_level_atom , { '+' , integer_lit } ;

universe_level_atom = integer_lit
                    | identifier                                (* level variable *)
                    | 'max'  , '(' , universe_level_expr
                                   , { ',' , universe_level_expr } , ')'
                    | 'imax' , '(' , universe_level_expr , ',' , universe_level_expr , ')'
                    | '(' , universe_level_expr , ')' ;
  • Type(0) : Type(1) : Type(2) : ... is the predicative hierarchy.
  • Prop : Type(1) is the universe of proof-irrelevant propositions.
  • imax(u, v) is impredicative max — 0 if v = 0, else max(u, v).
  • Level polymorphism uses universe u or u: Level in generics.

See language/universes.md.

Tensor types (shape-typed arrays)​

tensor_type_expr = 'tensor' , '<' , shape_params , '>' , type_expr ;
(* shape_params: comma-separated compile-time dimensions; each is an
   integer literal, a bound identifier of kind Nat, or a meta-arith
   expression. Equivalent generic form: Tensor<T, [d1, d2, ...]>. *)

Two equivalent forms:

let a: Tensor<Float32, [3, 224, 224]> = ...;
let b: tensor<3, 224, 224> Float32     = ...;

Backing representation is a single Type::Tensor { element, shape, strides }. Shape validation for reshape / matmul / broadcast is performed by tensor_shape_checker. See language/tensor-types.md.

Linearity on type definitions​

linearity_qualifier = 'linear' | 'affine' ;

Attaches to type_def (see §2.4). linear T must be consumed exactly once; affine T at most once. Unqualified types are unrestricted. The contagion rule propagates linearity up through fields/variants; see language/linearity.md.

Cubical / dependent​

path_type_expr     = 'Path' , type_args , '(' , expression , ',' , expression [, ','] , ')' ;
dependent_app_type = type_head , [ type_args ] ,
                     '(' , expression , { ',' , expression } , [ ',' ] , ')' ;
                     (* generalises Path<A>(a,b) to arbitrary dependent
                        type constructors indexed by runtime values:
                        Glue<A>(phi, T, e), IsContrMap<A, B>(f),
                        Fiber<A, B>(f, b), C.cells(0) *)
interval_endpoint  = 'i0' | 'i1' ;
genref_type        = 'GenRef' , '<' , type_expr , '>' ;
higher_kinded_type = path , '<' , '_' , '>' ;

Capability-restricted types​

capability_type = path_type , 'with' , capability_list ;
capability_list = '[' , capability_item , { ',' , capability_item } , ']' ;
capability_item = capability_name | capability_or_expr ;
capability_name = 'Read' | 'Write' | 'ReadWrite' | 'Admin' | 'Transaction'
                | 'Network' | 'FileSystem' | 'Query' | 'Execute'
                | 'Logging' | 'Metrics' | 'Config' | 'Cache' | 'Auth'
                | identifier ;
type Database.ReadOnly is Database with [Read];
fn analyse(db: Database with [Read]) -> Stats { ... }

Subtyping rule: T with [A, B, C] <: T with [A, B] when capabilities are a superset.

2.8 Protocols and implementations​

protocol_item     = protocol_function | protocol_type | protocol_const ;

protocol_function = visibility , function_modifiers , 'fn' , identifier , [ generics ]
                  , '(' , param_list , ')' , [ '->' , return_type_with_refinement ]
                  , [ context_clause ] , [ where_clause ] , [ default_impl ] ;

protocol_type     = 'type' , identifier , [ type_params ] , [ ':' , type_bounds ]
                  , [ where_clause ] , [ default_type ] , ';' ;

protocol_const    = 'const' , identifier , ':' , type_expr , ';' ;

(* Implementation block — supports specialization & default items *)
impl_block        = [ attribute ] , [ 'unsafe' ] , 'implement' , [ generics ] , impl_type
                  , [ where_clause ] , '{' , { impl_item } , '}' ;

impl_type         = type_expr , 'for' , type_expr     (* implement P for T *)
                  | type_expr ;                       (* implement T (inherent impl) *)

impl_item         = visibility , [ 'default' ] , ( function_def | type_alias | const_def ) ;

(* Associated type binding inside `implement` / `protocol` blocks.            *)
(* Distinct from the top-level `type_def` (§2.4) — only the associated-type   *)
(* binding uses `=`. Top-level type definitions ALWAYS use `is`.              *)
(*                                                                            *)
(* Example:                                                                   *)
(*   implement Iterator for Range {                                           *)
(*       type Item = Int;            (* this production *)                    *)
(*       fn next(&mut self) -> ... { ... }                                    *)
(*   }                                                                        *)
type_alias        = 'type' , identifier , [ type_params ] , [ ':' , type_bounds ]
                  , '=' , type_expr , ';' ;

2.9 Contexts​

Context definitions​

context_def      = visibility , ( 'context' , [ 'async' ] | 'async' , 'context' )
                 , identifier , [ generics ] , '{' , { context_item } , '}' ;

context_item     = context_function | context_type | context_const ;
context_function = visibility , [ 'async' ] , 'fn' , identifier , [ generics ]
                 , '(' , param_list , ')' , [ '->' , type_expr ]
                 , [ context_clause ] , ';' ;

Dual-kind context protocols​

(* Primary form *)
context_protocol_def      = visibility , 'context' , 'protocol' , identifier
                          , [ generics ] , protocol_body ;

(* Alternative (full symmetry with type defs) *)
context_type_protocol_def = visibility , 'context' , 'type' , identifier
                          , [ generics ] , [ meta_where_clause ]
                          , 'is' , 'protocol' , protocol_body , ';' ;

A context protocol can be used both as a type bound (T: Logger, 0 ns) and as an injectable context (using [Logger], 5–30 ns).

Context clauses (the using [...] system — 5 forms)​

context_clause      = 'using' , context_spec ;
context_spec        = single_context_spec | extended_context_list ;
single_context_spec = [ '!' ] , context_path , [ context_alias ] , [ context_condition ] ;

extended_context_list = '[' , extended_context_item , { ',' , extended_context_item } , ']' ;
extended_context_item = negative_context
                      | conditional_context
                      | transformed_context
                      | named_context
                      | simple_context ;

negative_context     = '!' , context_path ;                                 (* using [!IO] *)
conditional_context  = context_path , [ context_alias ] , 'if' , compile_time_condition ;
transformed_context  = context_path , context_transform , { context_transform } , [ context_alias ] ;
named_context        = identifier , ':' , context_path
                     | context_path , 'as' , identifier ;
simple_context       = context_path , [ context_alias ] ;

context_transform    = '.' , identifier , [ '(' , [ transform_args ] , ')' ] ;
context_alias        = 'as' , identifier ;
context_condition    = 'if' , compile_time_condition ;

compile_time_condition = config_condition       (* cfg.foo *)
                       | const_condition
                       | type_constraint_condition
                       | platform_condition
                       | boolean_condition ;
fn handler(req: Request) -> Response
    using [
        Database.transactional(),               // transformed
        Logger as primary,                      // aliased
        Analytics if cfg.analytics_enabled,     // conditional
        !Random,                                // negative — forbid Random
    ]
{ ... }

Context groups & provide​

context_group_def = 'using' , identifier , '=' , context_list_def , ';' ;

provide_stmt      = 'provide' , context_path , [ 'as' , identifier ] , '='
                  , expression , ( ';' | 'in' , block_expr ) ;
using Pure = [!IO, !State<_>, !Random];
provide Database = db in { fetch_user(id) };

2.10 FFI​

ffi_declaration = visibility , 'ffi' , identifier , [ 'extends' , identifier ]
                , '{' , ffi_items , '}' ;

ffi_item = ffi_function_decl
         | ffi_requires_clause
         | ffi_ensures_clause
         | ffi_memory_effects
         | ffi_thread_safety
         | ffi_error_protocol
         | ffi_ownership_spec ;

ffi_function_decl = '@extern' , '(' , string_lit , [ ',' , calling_convention_attr ] , ')' ,
                    'fn' , identifier , [ generics ] , '(' , param_list , ')' ,
                    [ '->' , type_expr ] , ';' ;

extern_block      = 'extern' , [ string_lit ] , '{' , { extern_fn_decl } , '}' ;

(* Boundary contracts *)
ffi_memory_effects = 'memory_effects' , '=' , memory_effect_spec , ';' ;
memory_effect_spec = 'Pure'
                   | 'Reads' , '(' , path , ')'
                   | 'Writes' , '(' , path , ')'
                   | 'Allocates'
                   | 'Deallocates' , '(' , path , ')'
                   | memory_effect_spec , '+' , memory_effect_spec ;

ffi_error_protocol = 'errors_via' , '=' , error_mechanism , ';' ;
error_mechanism    = 'None'
                   | 'Errno'
                   | 'ReturnCode' , '(' , pattern , ')'
                   | 'ReturnValue' , '(' , expression , ')' , [ 'with' , 'Errno' ]
                   | 'Exception' ;

ffi_ownership_spec = '@ownership' , '(' , ownership_mode , ')' ;
ownership_mode     = 'transfer_to' , '=' , string_lit
                   | 'transfer_from' , '=' , string_lit
                   | 'borrow'
                   | 'shared' ;

Every FFI boundary carries a typed contract — preconditions, postconditions, memory-effect annotations, thread-safety, error protocol, ownership transfer. See FFI.

2.11 Expressions​

The precedence ladder, top to bottom (loosest → tightest binding):

expression          = pipeline_expr ;

pipeline_expr       = assignment_expr , { '|>' , ( pipe_method_call | assignment_expr ) } ;
assignment_expr     = destructuring_assign | simple_assign ;

simple_assign       = null_coalesce_expr , [ assign_op , assignment_expr ] ;
null_coalesce_expr  = range_expr , { '??' , range_expr } ;
range_expr          = logical_or_expr , [ range_op , logical_or_expr ] ;
logical_or_expr     = logical_and_expr , { '||' , logical_and_expr } ;
logical_and_expr    = equality_expr , { '&&' , equality_expr } ;
equality_expr       = is_relational_expr , { ( '==' | '!=' ) , is_relational_expr } ;
is_relational_expr  = relational_expr , [ 'is' , [ 'not' ] , pattern ] ;
relational_expr     = bitwise_expr , { ( '<' | '>' | '<=' | '>=' ) , bitwise_expr } ;
bitwise_expr        = shift_expr , { ( '&' | '|' | '^' ) , shift_expr } ;
shift_expr          = additive_expr , { ( '<<' | '>>' ) , additive_expr } ;
additive_expr       = mult_expr , { ( '+' | '-' ) , mult_expr } ;
mult_expr           = power_expr , { ( '*' | '/' | '%' ) , power_expr } ;
power_expr          = unary_expr , [ '**' , power_expr ] ;       (* right-assoc *)

unary_expr          = unary_op , unary_expr | postfix_expr ;
unary_op            = '!' | '-' | '~'
                    | '&' | '&' , 'mut'
                    | '&' , 'checked' | '&' , 'checked' , 'mut'
                    | '&' , 'unsafe'  | '&' , 'unsafe'  , 'mut'
                    | '*' ;

postfix_expr        = primary_expr , { postfix_op } ;
postfix_op          = '.' , identifier , [ type_args ] , [ call_args ]
                    | '?.' , identifier , [ type_args ] , [ call_args ]
                    | '.' , integer_lit          (* tuple index *)
                    | '.' , 'await'
                    | '[' , expression , ']'
                    | [ type_args ] , call_args
                    | '?'                        (* propagation *)
                    | 'as' , type_expr ;
No chained comparisons

a < b < c parses as (a < b) < c (left-assoc) — a type error. Use a < b && b < c. The grammar deliberately rejects Python-style chains for predictability.

Destructuring assignment​

destructuring_assign = destructuring_target , assign_op , assignment_expr ;
destructuring_target = '(' , expression_list , ')'                   (* (a, b) = (b, a) *)
                     | '[' , expression_list , ']'                   (* [h, ..t] = list *)
                     | path , '{' , field_expr_list , '}'            (* Point { x, y } = pt *)
                     | '(' , destructuring_target , ')' ;

Primary expressions​

primary_expr = literal_expr
             | path_expr
             | '(' , ')'                          (* unit *)
             | '(' , expression , ')'             (* parens *)
             | tuple_expr
             | array_expr
             | tensor_literal_expr
             | map_expr | set_expr
             | comprehension_expr | map_comprehension | set_comprehension | generator_expr
             | stream_expr
             | record_expr
             | block_expr
             | if_expr | match_expr | loop_expr
             | try_expr
             | closure_expr
             | meta_expr | meta_call | meta_function | quote_expr
             | async_expr | unsafe_expr
             | return_expr | throw_expr
             | break_expr | continue_expr
             | spawn_expr | yield_expr
             | select_expr | nursery_expr
             | forall_expr | exists_expr
             | typeof_expr ;

Control flow​

if_expr        = 'if' , if_condition , block_expr
               , [ 'else' , ( if_expr | block_expr ) ] ;

(* if-let chains (RFC 2497 semantics) *)
if_condition   = let_condition , { '&&' , let_condition } ;
let_condition  = 'let' , pattern , '=' , expression | expression ;

match_expr     = [ expression , '.' ] , 'match' , [ expression ] , '{' , match_arms , '}' ;
match_arm      = { attribute } , pattern , [ guard ] , '=>' , expression ;
guard          = 'if' , expression | 'where' , expression ;

loop_expr      = infinite_loop | while_loop | for_loop | for_await_loop ;
while_loop     = 'while' , expression , { loop_annotation } , block_expr ;
for_loop       = 'for' , pattern , 'in' , expression , { loop_annotation } , block_expr ;
for_await_loop = 'for' , 'await' , pattern , 'in' , expression
               , { loop_annotation } , block_expr ;

loop_annotation = 'invariant' , expression | 'decreases' , expression ;

Closures​

closure_expr   = [ 'async' ] , closure_params , [ '->' , type_expr ] , expression ;
closure_params = '|' , [ param_list_lambda ] , '|' ;

Async / structured concurrency​

async_expr      = 'async' , block_expr ;
spawn_expr      = 'spawn' , [ 'using' , '[' , identifier_list , ']' ] , expression ;
yield_expr      = 'yield' , expression ;

select_expr     = 'select' , [ 'biased' ] , '{' , select_arms , '}' ;
select_arm      = { attribute } , pattern , '=' , await_expr , [ select_guard ] , '=>' , expression ;
await_expr      = expression , '.' , 'await' ;
select_else     = 'else' , '=>' , expression , [ ',' ] ;

nursery_expr    = 'nursery' , [ nursery_options ] , block_expr , [ nursery_handlers ] ;
nursery_options = '(' , nursery_option , { ',' , nursery_option } , ')' ;
nursery_option  = 'timeout' , ':' , expression
                | 'on_error' , ':' , ( 'cancel_all' | 'wait_all' | 'fail_fast' )
                | 'max_tasks' , ':' , expression ;
nursery_cancel  = 'on_cancel' , block_expr ;
nursery_recover = 'recover' , recover_body ;

Try / recover / finally​

try_expr        = 'try' , block_expr , [ try_handlers ] ;
try_handlers    = try_recovery , [ try_finally ] | try_finally ;
try_recovery    = 'recover' , recover_body ;
recover_body    = '{' , match_arms , '}'                  (* match-arm form *)
                | closure_params , recover_closure_body ; (* closure form *)
try_finally     = 'finally' , block_expr ;

Stream literals & comprehensions​

stream_expr     = stream_comprehension_expr | stream_literal_expr ;

comprehension_expr = '[' , expression , 'for' , pattern , 'in' , expression
                   , { comprehension_clause } , ']' ;
map_comprehension  = '{' , expression , ':' , expression , 'for' , pattern , 'in' , expression
                   , { comprehension_clause } , '}' ;
set_comprehension  = 'set' , '{' , expression , 'for' , pattern , 'in' , expression
                   , { comprehension_clause } , '}' ;
generator_expr     = 'gen'  , '{' , expression , 'for' , pattern , 'in' , expression
                   , { comprehension_clause } , '}' ;

comprehension_clause = 'for' , pattern , 'in' , expression
                     | 'let' , pattern , [ ':' , type_expr ] , '=' , expression
                     | 'if' , expression ;

stream_literal_expr  = 'stream' , '[' , stream_literal_body , ']' ;
stream_literal_body  = stream_range_body | stream_elements_body ;

Quote / staged metaprogramming​

quote_expr        = 'quote' , [ '(' , stage_level , ')' ] , '{' , token_tree , '}' ;
quote_interpolation = splice_operator , ( identifier | '{' , expression , '}' ) ;
splice_operator     = '$' , { '$' } ;       (* one $ per stage level escaped *)
quote_repetition    = splice_operator , '[' , 'for' , pattern , 'in' , expression , '{' , token_tree , '}' , ']' ;
quote_stage_escape  = '$' , '(' , 'stage' , stage_level , ')' , '{' , expression , '}' ;
quote_lift          = 'lift' , '(' , expression , ')' ;

$var splices into the immediate enclosing quote (stage N−1); $$var into the parent (N−2); $$$var into N−3; and so on.

Quantifiers (specifications & proofs)​

forall_expr = 'forall' , quantifier_binding , { ',' , quantifier_binding } , '.' , expression ;
exists_expr = 'exists' , quantifier_binding , { ',' , quantifier_binding } , '.' , expression ;

quantifier_binding =
    pattern , [ ':' , type_expr ] , [ 'in' , expression ] , [ 'where' , expression ] ;

Three forms supported: type-based, collection-based, combined.

typeof and pattern test​

typeof_expr        = 'typeof' , '(' , expression , ')' ;     (* runtime type info *)
is_relational_expr = relational_expr , [ 'is' , [ 'not' ] , pattern ] ;

2.12 Patterns​

pattern         = or_pattern ;
or_pattern      = guarded_pattern , { '|' , guarded_pattern } ;
guarded_pattern = and_pattern , [ guard ] ;
and_pattern     = primary_pattern , { '&' , primary_pattern } ;
primary_pattern = simple_pattern | active_pattern ;

simple_pattern  = literal_pattern
                | type_test_pattern
                | identifier_pattern
                | wildcard_pattern
                | rest_pattern
                | tuple_pattern
                | array_pattern
                | slice_pattern
                | stream_pattern
                | record_pattern
                | variant_pattern
                | reference_pattern
                | range_pattern ;

type_test_pattern  = identifier , 'is' , type_expr ;
identifier_pattern = [ 'ref' ] , [ 'mut' ] , identifier , [ '@' , pattern ] ;
wildcard_pattern   = '_' ;
rest_pattern       = '..' ;
slice_pattern      = '[' , slice_pattern_elements , ']' ;
slice_pattern_elements = [ pattern , { ',' , pattern } , ',' ] , '..'
                       , [ ',' , pattern , { ',' , pattern } ] ;
stream_pattern     = 'stream' , '[' , stream_pattern_elements , ']' ;
record_pattern     = path , '{' , field_patterns , '}' ;
variant_pattern    = path , [ variant_pattern_data ] ;
variant_pattern_data = '(' , pattern_list , ')' | '{' , field_patterns , '}' ;
reference_pattern  = '&' , [ 'mut' ] , pattern ;
range_pattern      = literal_expr , range_op , [ literal_expr ]
                   | range_op , literal_expr ;

Active patterns (F#-style)​

active_pattern        = identifier , active_pattern_tail ;
active_pattern_tail   = '(' , ')'                                   (* total, no params *)
                      | '(' , ')' , '(' , pattern_list_nonempty , ')'  (* partial, no params *)
                      | '(' , expression_list , ')' , '(' , [ pattern_list ] , ')' ; (* with params *)

pattern_def           = visibility , 'pattern' , identifier , [ pattern_type_params ]
                      , '(' , pattern_params , ')' , '->' , type_expr , '=' , expression , ';' ;

Total patterns return Bool; partial patterns return Maybe<T> for extraction.

2.13 Statements​

statement       = let_stmt
                | let_else_stmt
                | provide_stmt
                | item
                | defer_stmt
                | expression_stmt ;

let_stmt        = 'let' , pattern , [ ':' , type_expr ] , [ '=' , expression ] , ';' ;
let_else_stmt   = 'let' , pattern , '=' , expression , 'else' , block_expr ;
defer_stmt      = 'defer' , defer_body | 'errdefer' , defer_body ;
defer_body      = expression , ';' | block_expr ;
expression_stmt = expression , [ ';' ] ;

2.14 Constants and statics​

const_def  = visibility , 'const'  , identifier , ':' , type_expr , '=' , const_expr , ';' ;
static_def = visibility , 'static' , [ 'mut' ] , identifier , ':' , type_expr , '=' , const_expr , ';' ;

2.15 Metaprogramming​

meta_def        = visibility , 'meta' , identifier , meta_args , '{' , meta_rules , '}' ;
meta_args       = '(' , [ meta_params_meta ] , ')' ;
meta_param_def  = identifier , [ ':' , meta_fragment ] ;
meta_fragment   = 'expr' | 'stmt' | 'type' | 'pattern' | 'ident'
                | 'path' | 'tt' | 'item' | 'block' ;

meta_rules      = meta_rule , { '|' , meta_rule } ;
meta_rule       = pattern , '=>' , expression ;

(* Macro invocation — @ prefix only *)
meta_call       = '@' , path , meta_call_args ;
meta_call_args  = '(' , [ argument_list ] , ')'
                | '[' , token_tree , ']'
                | '{' , token_tree , '}' ;

(* Built-in compile-time functions *)
meta_function      = '@' , meta_function_name , [ '(' , [ argument_list ] , ')' ] ;
meta_function_name = 'const' | 'error' | 'warning' | 'stringify' | 'concat' | 'cfg'
                   | 'file' | 'line' | 'column' | 'module' | 'function'
                   | 'type_name' | 'type_fields' | 'field_access'
                   | 'type_of' | 'fields_of' | 'variants_of'
                   | 'is_struct' | 'is_enum' | 'is_tuple' | 'implements' ;

@-prefix parsing priority (resolved by the parser):

  1. @name item … → attribute_item
  2. @name(args) / @name[…] / @name{…} → meta_call
  3. @builtin (where builtin ∈ {const, cfg, file, …}) → meta_function
  4. bare @name → at_literal

2.16 Type properties (compile-time introspection)​

type_property_expr = type_expr , '.' , type_property_name ;
type_property_name = 'size' | 'alignment' | 'stride'
                   | 'min'  | 'max'       | 'bits'
                   | 'name' | 'id' ;
const PTR_SIZE: Int = (&Int).size;            // 16 (ThinRef)
const FLOAT_ALIGN: Int = Float.alignment;     // 8

Replaces deprecated intrinsic functions (size_of<T>(), etc.).

2.17 Built-in functions (no ! suffix)​

builtin_call         = builtin_name , '(' , [ argument_list ] , ')' ;
builtin_io           = 'print' | 'eprint' ;
builtin_assertion    = 'assert' | 'assert_eq' | 'assert_ne' | 'debug_assert' ;
builtin_control_flow = 'panic' | 'unreachable' | 'unimplemented' | 'todo' ;
builtin_async        = 'join' | 'try_join' | 'join_all' | 'select_any' | 'ready' | 'pin' ;
builtin_name         = builtin_io | builtin_assertion | builtin_control_flow | builtin_async ;

These are functions, not macros. print(f"x = {x}") — never print!().

2.18 Formal proofs and verification (Section 2.19 in the EBNF)​

theorem_decl   = 'theorem'   , identifier , [ generic_params ] , '(' , [ param_list ] , ')'
               , [ '->' , type_expr ] , [ requires_clause ] , [ ensures_clause ] , proof_body ;
lemma_decl     = 'lemma'     , identifier , [ generic_params ] , '(' , [ param_list ] , ')'
               , [ '->' , type_expr ] , [ requires_clause ] , [ ensures_clause ] , proof_body ;
axiom_decl     = 'axiom'     , identifier , [ generic_params ] , '(' , [ param_list ] , ')'
               , [ '->' , type_expr ]
               , [ requires_clause ]
               , [ ensures_clause ]
               , [ where_clause ]
               , ';' ;
ensures_clause = 'ensures' , expression , { ',' , expression } ;

(* Axioms may also appear inside protocol bodies (T1-R) — they become
   proof obligations at every `implement` site, realising the
   model-theoretic semantics of protocols: an implementation IS a
   model of the theory iff every axiom holds on its concrete ops. *)
protocol_item_axiom = axiom_decl ;
corollary_decl = 'corollary' , identifier , [ generic_params ] , '(' , [ param_list ] , ')'
               , [ '->' , type_expr ] , [ requires_clause ] , 'from' , identifier , proof_body ;
tactic_decl    = 'tactic'    , identifier , [ generic_params ]
               , '(' , [ tactic_param_list ] , ')'
               , [ where_clause ] , tactic_body ;

tactic_param_list = tactic_param , { ',' , tactic_param } ;
tactic_param      = identifier , ':' , tactic_param_type
                    , [ '=' , expression ] ;
tactic_param_type = 'Expr' | 'Type' | 'Tactic' | 'Hypothesis' | 'Int'
                  | 'Prop' | type_expr ;

tactic_body       = tactic_expr | '{' , { tactic_stmt } , '}' ;
tactic_stmt       = 'let'   , identifier , [ ':' , type_expr ] , '=' , expression , ';'
                  | 'if'    , expression , '{' , tactic_expr , '}'
                    , [ 'else' , ( 'if' , expression , '{' , tactic_expr , '}' , …
                                 | '{'  , tactic_expr , '}' ) ]
                  | 'match' , expression , '{' , match_arm , { ( ',' | ';' ) , match_arm } , [ ',' | ';' ] , '}'
                  | 'fail'  , '(' , expression , ')'
                  | tactic_expr , [ ';' ] ;

requires_clause = 'requires' , expression , { ',' , expression } ;

proof_body       = 'proof' , ( proof_by_tactic | proof_by_term | proof_structured ) ;
proof_by_tactic  = 'by' , tactic_expr ;
proof_by_term    = '=' , expression ;
proof_structured = '{' , { proof_step } , '}' ;

proof_step          = have_step | show_step | obtain_step | calc_chain | tactic_application ;
have_step           = 'have'   , identifier , ':' , expression , proof_justification ;
show_step           = 'show'   , expression , proof_justification ;
obtain_step         = 'obtain' , pattern , 'from' , expression ;
tactic_application  = tactic_expr , ';' ;
proof_justification = 'by' , ( tactic_expr | identifier ) ;

(* Tactic combinators — see Verification → Tactic DSL *)
tactic_expr = tactic_name , [ type_args ] , [ '(' , [ argument_list ] , ')' ]
            | tactic_expr , ';' , tactic_expr
            | '(' , tactic_expr , ')'
            | 'try' , '{' , tactic_expr , '}' , [ 'else' , '{' , tactic_expr , '}' ]
            | 'repeat' , [ '(' , integer_lit , ')' ] , '{' , tactic_expr , '}'
            (* `first` supports BOTH the block form and the Lean-style list form *)
            | 'first' , '{' , tactic_expr , { ';' , tactic_expr } , '}'
            | 'first' , '[' , tactic_expr , { ',' , tactic_expr } , ']'
            | 'all_goals' , '{' , tactic_expr , '}'
            | 'focus' , '(' , integer_lit , ')' , '{' , tactic_expr , '}' ;

tactic_name = 'auto' | 'simp' | 'ring' | 'field' | 'omega' | 'blast' | 'smt'
            | 'trivial' | 'assumption' | 'contradiction' | 'induction' | 'cases'
            | 'rewrite' | 'unfold' | 'apply' | 'exact' | 'intro' | 'intros'
            | 'cubical' | 'category_simp' | 'category_law' | 'descent_check'
            | identifier ;

(* Calculational chains *)
calc_chain    = 'calc' , '{' , calc_step , { calc_step } , '}' ;
calc_step     = expression , calc_relation , '{' , proof_justification , '}' , expression ;
calc_relation = '==' | '<' | '<=' | '>' | '>=' | '!=' ;
theorem sum_first_n(n: Int { self >= 0 })
    -> sum(0..=n) == n * (n+1) / 2
{
    proof by induction n {
        case 0 => qed;
        case k + 1 => calc {
            sum(0..=k+1)
          == { by def sum }   sum(0..=k) + (k+1)
          == { by ih }        k*(k+1)/2 + (k+1)
          == { by ring }      (k+1)*(k+2)/2 ;
        };
    }
}

Layer 3 — Error Recovery​

The parser's recovery strategies are encoded in the grammar so tooling behaves consistently across implementations.

error_recovery  = synchronize_on_semicolon
                | synchronize_on_brace
                | synchronize_on_keyword
                | insert_missing_delimiter
                | skip_invalid_tokens ;

synchronize_on_semicolon = { token - ';' } , ';' ;
synchronize_on_brace     = { token - '}' } , '}' ;
synchronize_on_keyword   = { token - keyword } , keyword ;

insert_missing_delimiter = insert_semicolon | insert_closing_brace | insert_closing_paren ;

unclosed_delimiter_error = '(' , { token - ')' } , end_of_file
                         | '[' , { token - ']' } , end_of_file
                         | '{' , { token - '}' } , end_of_file ;

Recovery points: ;, }, {, fn, type, implement, module, mount. The parser skips tokens until reaching one and resumes, emitting one diagnostic per recovery (no cascades).

Cross-references​

If you want to read about…See
Friendly walkthrough of these productionsLanguage → Syntax
Type-system surfaceLanguage → Types, Refinement types, Dependent types
Patterns in depthLanguage → Patterns
Functions, contractsLanguage → Functions
References, CBGRLanguage → References, CBGR
Context system semanticsLanguage → Context system
Async / nursery / selectLanguage → Async
Macro / quote systemLanguage → Metaprogramming
FFI boundary contractsLanguage → FFI
Proof DSL semanticsVerification → Proofs
Operator precedence tableReference → Operators
Full keyword indexReference → Keywords
Attribute semanticsReference → Attribute registry

Tooling​

verum grammar dump            # render railroad diagrams
verum grammar search <rule>   # locate a production
verum grammar validate FILE   # validate a .vr file against the grammar only
verum disasm --show-tokens    # tokeniser output for debugging

Version​

This page reflects grammar version 3.0 — 2,423 lines of EBNF. Future revisions will be announced on the blog and cross-linked here.