AGDA
Generated by scripts/gen-format-pages.py from docs/data/format-metadata/, FILE_FORMATS.csv and docs/formats-master.csv. Do not edit by hand: change the source, then run the script.
Agda Preview.
At a glance
| Purpose | Agda source code: modules, data types, records, postulates and the definitions and proofs of the dependently typed language. |
| Extensions | .agda |
| Poka parser | poka-agda |
| Viewer | poka-metadata-card-viewer |
| Depth tier | Metadata card (see Depth tiers) |
| Breadth tier | B4 Summary (see Breadth tiers) |
How much Poka reads
B4 Summary. The container and metadata are read and summarised (counts, properties, structure), but the main content is not rendered.
Confidence: medium (the reviewer read the code). Basis: Reviewed 2026-10-26: read parsers/poka-agda/src/main.rs (302 lines) and plugin.json in full. The crate has no unit tests and no tests/samples.rs, and the corpus has no .agda sample, so the tier rests on reading the code. Covers .agda. The output is a metadata card of counts found by matching text line by line: the module name, imports, data and record declarations, postulate blocks, private modules, type signatures, bindings, with patterns, rewrite uses, pragmas, literate prose lines and line counts. Judgement: B4, because the structure is summarised but the source itself is never shown.
What Poka does not read
- The source text is not shown: the card carries only counts and a few sample names, with no code view or highlighting
- Constructs are found by matching text line by line, not by parsing, so multi-line declarations, nested or indented definitions and keywords inside strings or comments can be miscounted
- Counts of named items stop where their name list is capped (imports at 32, datas at 32, records at 32), so a larger file under-reports them
- Files over 32 MiB are cut to the first 32 MiB (the card says so)
- Text that is not UTF-8 is decoded with replacement characters; no other encoding is tried
- Literate Agda (.lagda, .lagda.md) is handled in the code but not routed: the manifest claims only .agda
Libraries
Libraries Poka uses or has assessed for this format, with the status, licence and language the registry records.
- tree-sitter-agda (candidate; MIT; JavaScript/C; https://github.com/tree-sitter/tree-sitter-agda) — Tree-sitter grammar (grammar.js); Rust bindings present in the repository; suited to highlighting rather than full semantic parsing
Sources
- parsers/poka-agda/src/main.rs
- parsers/poka-agda/plugin.json