Category: coq

Posts in this Category (2)

Extraction in Coq

Published on: May 31, 2016

Extraction erases Props Extraction in Coq works by erasing Props. For example, consider the following definition of div: Definition div (m n : nat)(H : n<>0): nat := NPeano.div m n. div expects a proof that its second argument is non-zero. Indeed, in coq, it is impossible for div to...

Coq Basics

Published on: April 09, 2014

GADTs vs Inductive Datatypes Consider the following definition of Nat-indexed Vector GADT in OCaml and Haskell: OCaml: (* vec : * -> * -> * *) type (_,_) vec = | Nil : ('a,zero) vec | Cons : 'a * ('a,'b) vec -> ('a,'b succ) vec Haskell: data Vec ::...