Embed Lean in Clojure.
deflean takes Lean source, checks it (including every proof) with lake build at macro-expansion time, and defines the Lean functions in the current
namespace through code generated by the lean-clj CLI.
Embed Lean in Clojure. `deflean` takes Lean source, checks it (including every proof) with `lake build` at macro-expansion time, and defines the Lean functions in the current namespace through code generated by the `lean-clj` CLI.
Directory of the lake workspace and the generated-code cache.
Directory of the lake workspace and the generated-code cache.
(deflean block & args)Define the functions of a block of Lean in the current namespace.
(deflean arith (def double [n Nat] Nat (+ n n))
(theorem double_eq [n Nat] (= (double n) (* 2 n))
(by (unfold double) omega)))
The body is a sequence of lean-clj.dsl commands; a string in the body is
Lean source taken as is. An optional map before the body takes :imports,
a vector of Lean modules to import. The block becomes the Lean module
returned by module-name, whose definitions are wrapped in a namespace of
the same name. Lean checks the whole block, proofs included, when the macro
expands; a rejected block stops compilation with Lean's messages.
Define the functions of a block of Lean in the current namespace.
(deflean arith
(def double [n Nat] Nat
(+ n n))
(theorem double_eq [n Nat] (= (double n) (* 2 n))
(by (unfold double) omega)))
The body is a sequence of `lean-clj.dsl` commands; a string in the body is
Lean source taken as is. An optional map before the body takes `:imports`,
a vector of Lean modules to import. The block becomes the Lean module
returned by `module-name`, whose definitions are wrapped in a namespace of
the same name. Lean checks the whole block, proofs included, when the macro
expands; a rejected block stops compilation with Lean's messages.(expand ns-name block opts src)Clojure forms for the deflean block block in ns-name, given its Lean
source. Generated code is cached in *workspace*/cache under a hash of the
inputs.
Clojure forms for the deflean block `block` in `ns-name`, given its Lean source. Generated code is cached in `*workspace*`/cache under a hash of the inputs.
Part of the cache key, so that cached output is regenerated when the generator changes.
Part of the cache key, so that cached output is regenerated when the generator changes.
(module-name ns-name block)Lean module of the block block in the Clojure namespace ns-name.
Lean module of the block `block` in the Clojure namespace `ns-name`.
(options opts body)deflean options with Clj imported when the body translates Clojure
functions.
deflean options with `Clj` imported when the body translates Clojure functions.
(source body)(source ns body extern?)Lean source of a deflean body in the namespace ns: strings are Lean
source (dedented), (clojure f ...) is the models of lean-clj.typed/defn
functions, and other forms are commands of lean-clj.dsl, whose structures
and enumerations are recorded in lean-clj.types/types.
Lean source of a deflean body in the namespace `ns`: strings are Lean source (dedented), `(clojure f ...)` is the models of `lean-clj.typed/defn` functions, and other forms are commands of `lean-clj.dsl`, whose structures and enumerations are recorded in `lean-clj.types/types`.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |