MODULES.adoc

Syntax Modules (Opt-in)

Table of Contents

• Module 0: Core (mandatory)
• Module 1: References
• Module 2: Figures and Tables
• Module 3: Inline Styling
• Module 4: Footnotes
• Module 5: Attributes
• Module 6: Constraints

A2ML is modular. The core stays small; additional modules add features. Modules only extend the surface syntax. The typed core is shared.

Module 0: Core (mandatory)

• Headings, paragraphs, lists, code fences

• Directives: @abstract, @refs, @opaque

Module 1: References

Adds IDs and explicit references.

Directive  ::= "@" Name Attrs? ":" NL DirectiveBody "@end"
Attrs      ::= "(" Attr ("," Attr)* ")"
Attr       ::= "id" "=" ID | "ref" "=" ID
InlineRef  ::= "@ref(" ID ")"

Semantics: all refs must resolve in checked/attested modes; IDs must be unique.

Module 2: Figures and Tables

Adds @fig and @table blocks with captions.

Semantics: captions required; optional policy that figures must be referenced.

Module 3: Inline Styling

Adds emphasis, strong, and links.

Semantics: presentational only.

Module 4: Footnotes

Adds footnote references and definitions.

Semantics: footnote refs must resolve in checked/attested modes.

Module 5: Attributes

Adds Djot-style attribute blocks for metadata and styling.

Semantics: attributes map to metadata; no invariants unless declared.

Module 6: Constraints

Adds explicit requirements with @requires(…​).

Semantics: requirements become proof obligations in attested mode.