Sqlite3 bindings for lean4 (mirror)
import FFI def double (f : Nat -> Nat) n := f (f n) def inc := fun n => n + 1 def main : IO Unit := IO.println s!"Hello, {double inc 100} {myAdd 1 1} {myAdd 1 1} {myAdd 1 1}"