弹药
发表于 2025-4-1 03:17:37
Automatically Proving Equivalence by Type-Safe Reflection,d. For example, implementing an adder for binary numbers indexed over their natural number equivalents naturally leads to proof obligations for equalities of expressions over natural numbers. The need for these equality proofs comes, in intensional type theories, from the fact that the propositional