Search

• < Previous
• 1
• Next >

An extensible equality checking algorithm for dependent type theories

We present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying extensionality rules and a normalization phase based on computation rules, where both kinds of rules are defined using the&nbsp;[&hellip;]