Sciweavers

ITP
2010
172views Mathematics» more  ITP 2010»
14 years 3 months ago
Equations: A Dependent Pattern-Matching Compiler
Abstract. We present a compiler for definitions made by pattern matching on inductive families in the Coq system. It allows to write structured, recursive dependently-typed functi...
Matthieu Sozeau