Sciweavers

ITP
2010
172views Mathematics» more  ITP 2010»
13 years 8 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