Encoding SAT in OCaml GADTs

I had some fun and wrote a post about a SAT → GADT encoding. Hope you enjoy!

6 Likes

Your code examples will fail to work starting with OCaml 5.5 because you are relying on the special handling of abstract types for the type true_ and false_ in the local module. Would you mind amending them to

type true_ = private Tag_true
type false_ = private Tag_false

(or any other distinguishable type declarations) ?

Updated the post! Thanks!