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 and mutually
recursive ones in mutual, with the Lean modules they need. 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 and mutually recursive ones in `mutual`, with the Lean modules they need. 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?)(clojure f ...) in the namespace ns: :text, the Lean source of the
models of the named functions and of the functions they call (@[extern] to
the Clojure vars with extern?), and :modules, the Lean modules they
need.
`(clojure f ...)` in the namespace `ns`: `:text`, the Lean source of the models of the named functions and of the functions they call (`@[extern]` to the Clojure vars with `extern?`), and `:modules`, the Lean modules they need.
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 |