Scope

semantic-explanation formalizes a domain-configurable route from reflected Agda terms to human-readable explanations. It represents propositions and expressions in a semantic intermediate representation that records binders, surface forms, and provenance. Domain specifications classify entity, predicate, expression, and infrastructure heads, while discourse profiles supply controlled statement labels and entity references. Reflection modules expose application spines and dependent function structure and restrict reduction to an explicit whitelist. Translation, realization, and macro modules connect those pieces into selectable explanation families for declarations.

Most important results

The translator handles atoms, equalities, implications, universal binders, and closed terms, returning structured failures by phase, tag, path, detail, and attempted rules. Translation preserves provenance for rules, unfolded aliases, and omitted binders or arguments. Realization offers canonical, compact, evidence-oriented, structured, and domain-evidence renderings, groups them into candidate sets, and supports selection by candidate identifier. The reflection macros expose fuel-bounded entry points for explaining names and report translation or candidate-selection failures through Agda’s type-checking interface.