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: the
environment variable LEAN_CLJ_WORKSPACE, or .lean-clj/ of the project
root (the nearest directory with a deps.edn).
Directory of the lake workspace and the generated-code cache: the environment variable `LEAN_CLJ_WORKSPACE`, or `.lean-clj/` of the project root (the nearest directory with a `deps.edn`).
(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, and :use, a vector of other blocks
(ns/block, or block of this namespace) whose definitions the block
uses. 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, located in this file.
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, and `:use`, a vector of other blocks
(`ns/block`, or `block` of this namespace) whose definitions the block
uses. 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, located in this file.(expand ns-name block opts src)(expand ns-name block opts src where)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
Lean module and of the deflean modules it imports. where locates the block
in its Clojure file for error messages.
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 Lean module and of the deflean modules it imports. `where` locates the block in its Clojure file for error messages.
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 ns opts body)deflean options in the namespace ns: :use of other blocks (ns/block,
or block of the same namespace) becomes imports and opens of their
modules, and a body that translates Clojure functions imports Clj.
deflean options in the namespace `ns`: `:use` of other blocks (`ns/block`, or `block` of the same namespace) becomes imports and opens of their modules, and a body that translates Clojure functions imports `Clj`.
(render ns block body extern?)The body of deflean block block in the namespace ns: :source, its
Lean source, :modules, the Lean modules of the functions from Lean that
translated functions call, and :parts, the source of each form. Strings
are Lean source (dedented), (clojure f ...) is the models of
lean-clj.typed/defn functions (@[extern] to the Clojure vars with
extern?), and other forms are commands of lean-clj.dsl, whose structures
and enumerations are recorded in lean-clj.types/types.
The body of deflean block `block` in the namespace `ns`: `:source`, its Lean source, `:modules`, the Lean modules of the functions from Lean that translated functions call, and `:parts`, the source of each form. Strings are Lean source (dedented), `(clojure f ...)` is the models of `lean-clj.typed/defn` functions (`@[extern]` to the Clojure vars with `extern?`), and other forms are commands of `lean-clj.dsl`, whose structures and enumerations are recorded in `lean-clj.types/types`.
(source ns block body extern?)The Lean source of render.
The Lean source of `render`.
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 |