Equality Checking for General Type Theories in Andromeda 2

摘要

We designed a user-extensible judgemental equality checking algorithm for general type theories that supports computation rules and extensionality rules. The user needs only provide the equality rules they wish to use, after which the algorithm devises an appropriate notion of normal form. The algorithm is a generalization of type-directed equality checking for Martin-Loef type theory, and we implemented it in the Andromeda 2 prover.