Queries.v has two ways to encode SQL queries in the language (with some helper functions).
I've also added a few optimizations to fuse fold and flatmap.
I needed to add a few lemmas about decidable equality of string/bool/ascii, which I'm told should probably eventually be moved to Coqutil (they're currently still in Optimize.v).
Queries.v has two ways to encode SQL queries in the language (with some helper functions). I've also added a few optimizations to fuse fold and flatmap. I needed to add a few lemmas about decidable equality of string/bool/ascii, which I'm told should probably eventually be moved to Coqutil (they're currently still in Optimize.v).