#+TITLE: Coq

 - [[./hlist-shallow.v][hlist.shallow.v]]: hlist with normal list under the hood
 - [[./hlist.v][hlist.v]]: Hlist (with notations)
 - [[./union.v][union.v]]: Mimicking a set operation using lists
 - [[./bv.v][bv.v]]: Demo of a few bitvector operations
 - [[./sumn.v][sumn.v]]: Sum of first n natural numbers, their squares and cubes.
 - [[./de-morgan.v][de-morgan.v]]: de-Morgan's laws
 - [[./odd-even-prop.v][odd-even-prop.v]]: Parity of ~nat~ values
 - [[./ltac2-demo.v][ltac2-demo.v]]: 'Hello world' with Ltac2
 - [[./inf-proof.v][inf-proof.v]]: A trivial proof involving streams (ie, infinite lists)
 - [[./3-way-mutrec.v][3-way-mutrec.v]]: An example of a 3-way mutually recursive function
 - [[./iseven-proof-mode.v][iseven-proof-mode.v]]: An ~iseven~ function defined only using proof mode
 - [[./cpdt/][cpdt/]]: stuff from the book CPDT
   + [[./cpdt/ilist.v][ilist.v]]: Length indexed lists
   + [[./cpdt/exercises.v][exercises.v]]: a few of the old exercises from cpdt
 - [[./sf/][sf]]: stuff from /Software foundations/
 - [[./third-party/][Snippets using third party libraries]]
   + [[./third-party/eqns.v][eqns.v]]: A 'hello world' using the 'equations' plugin
   + [[./third-party/extlib-hlist.v][extlib-hlist.v]]: Hlist using coq-ext-lib library