Type: adaptive · Priority: must
README/ECOSYSTEM describe a "language-agnostic engine", but the extension (.agda), import grammar (open import … hiding/using/as), the --safe --without-K pragma, postulate/-- JUSTIFY:, headline grammar, and root discovery (All.agda/Smoke.agda) are all hardcoded for Agda (src/graph.rs, src/lint/*, src/agda.rs). Until the Language abstraction lands, correct the docs to say Agda-first; multi-prover is the v0.2 boundary.
Type: adaptive · Priority: must
README/ECOSYSTEM describe a "language-agnostic engine", but the extension (
.agda), import grammar (open import … hiding/using/as), the--safe --without-Kpragma,postulate/-- JUSTIFY:, headline grammar, and root discovery (All.agda/Smoke.agda) are all hardcoded for Agda (src/graph.rs,src/lint/*,src/agda.rs). Until theLanguageabstraction lands, correct the docs to say Agda-first; multi-prover is the v0.2 boundary.