Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations
Abstract
We propose a generic approach to make arithmetic decision procedures designed for the concrete data-type Z of Coq available for alternative representations of integers. It is based on a transfer tool recently developped by Zimmermann and Herbelin to perform automatic and transparent transfer of theorems along isomorphisms.
Domains
Computer Science [cs]
Origin : Files produced by the author(s)
Loading...