HarvardPL / formulog

Datalog with support for SMT queries and first-order functional programming
https://harvardpl.github.io/formulog/
Apache License 2.0
155 stars 10 forks source link

Add tutorial (refinement type checking) #88

Closed aaronbembenek closed 1 month ago

aaronbembenek commented 1 month ago

This PR adds a tutorial that walks through using Formulog to implement a refinement type checker. Likely it would benefit from additional explanations and examples, but it does address some of the pain points identified by @bubaflub, and hopefully it'll be a good starting point for additional documentation.

Resolves #9