Type: adaptive · Priority: intend (epic; likely a 0.2 breaking change)
A Language trait/enum carrying: file extensions, import grammar, comment/pragma markers, root-discovery patterns, and tool-binary name. Refactor graph.rs (module_name_of, direct_imports, discover_roots), the pragma/postulate/escape-hatch rules, and agda.rs/unused.rs to dispatch through it. Prove it out with a second backend — Idris2 (estate-relevant via proven/ABIs) or Lean 4. This is what makes the language-agnostic claim true.
Type: adaptive · Priority: intend (epic; likely a 0.2 breaking change)
A
Languagetrait/enum carrying: file extensions, import grammar, comment/pragma markers, root-discovery patterns, and tool-binary name. Refactorgraph.rs(module_name_of,direct_imports,discover_roots), the pragma/postulate/escape-hatch rules, andagda.rs/unused.rsto dispatch through it. Prove it out with a second backend — Idris2 (estate-relevant viaproven/ABIs) or Lean 4. This is what makes the language-agnostic claim true.