Lean models of Clojure functions defined with lean-clj.typed/defn.
models turns the :lean/sig of each function into lean-clj.dsl
commands: a def whose body is the Clojure body written with the models of
clojure.core in Clj. Lean infers the types; the translation only follows
the syntax.
Lean models of Clojure functions defined with `lean-clj.typed/defn`. `models` turns the `:lean/sig` of each function into `lean-clj.dsl` commands: a `def` whose body is the Clojure body written with the models of `clojure.core` in `Clj`. Lean infers the types; the translation only follows the syntax.
(clojure-command? x)Whether x is the deflean command (clojure f ...).
Whether `x` is the deflean command `(clojure f ...)`.
(models vs extern?)lean-clj.dsl commands of the Lean models of the lean-clj.typed/defn
vars vs and of the functions they call, callees first. With extern?, each
model is @[extern] to its Clojure var, so that compiled Lean calls the
Clojure function.
`lean-clj.dsl` commands of the Lean models of the `lean-clj.typed/defn` vars `vs` and of the functions they call, callees first. With `extern?`, each model is `@[extern]` to its Clojure var, so that compiled Lean calls the Clojure function.
(render-command ns [_ & syms :as cmd] extern?)Lean source of (clojure f ...) in the namespace ns: the models of the
named functions and of the functions they call, @[extern] to the Clojure
vars.
Lean source of `(clojure f ...)` in the namespace `ns`: the models of the named functions and of the functions they call, `@[extern]` to the Clojure vars.
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 |