Lean4 SQL Utils
This repository is a collection of utilities that were split off from lean4 sql initiatives such as (LeanMySQL, lean-postgres) as they could be shared across different dialects.
Installation
Lake
Add the following dependency to your lakefile.lean
:
package your-package where
dependencies := #[{
name := `«sql-utils»
src := Source.git "https://github.com/FWuermse/lean4-sql-utils" "main"
}]
Usage
Currently the main feature includes built in query syntax that can be used the following way:
import SqlUtils.SQLSyntax
def main : IO Unit := do
let query :=
SELECT name, age, height, job_name
FROM person LEFT JOIN job ON person.job_id = job.id
WHERE person.age > 20
IO.println query
Contributing
Contributions are always welcome. Please refer to the Lean4 Contributing Guidelines and their commit convention.