Lean types written as lean-clj.dsl terms, and what lean-clj derives from
them: test.check generators of the Clojure values that correspond to a type,
a check of such values, malli schemas, and clj-kondo types.
Structures and enumerations are known by the Lean name they are written
with in a deflean block (register-commands!).
Lean types written as `lean-clj.dsl` terms, and what lean-clj derives from them: test.check generators of the Clojure values that correspond to a type, a check of such values, malli schemas, and clj-kondo types. Structures and enumerations are known by the Lean name they are written with in a `deflean` block (`register-commands!`).
(fn-schema v)malli function schema [:=> [:cat T ...] R] of a lean-clj.typed/defn
var, for malli.core/=>.
malli function schema `[:=> [:cat T ...] R]` of a `lean-clj.typed/defn` var, for `malli.core/=>`.
(gen t)test.check generator of the Clojure values of the Lean type t.
test.check generator of the Clojure values of the Lean type `t`.
(kebab s)Clojure name of a Lean name component, as the generated code writes it
(ownerName → owner-name).
Clojure name of a Lean name component, as the generated code writes it (`ownerName` → `owner-name`).
(kondo-config nss)clj-kondo :type-mismatch config of the lean-clj.typed/defn functions
in the namespaces nss.
clj-kondo `:type-mismatch` config of the `lean-clj.typed/defn` functions in the namespaces `nss`.
(kondo-type t)clj-kondo type of the Clojure values of the Lean type t.
clj-kondo type of the Clojure values of the Lean type `t`.
(malli-schema t)malli schema of the Clojure values of the Lean type t, as data.
malli schema of the Clojure values of the Lean type `t`, as data.
(register-commands! cmds)Record the monomorphic structures and enumerations among lean-clj.dsl
commands. Each is also known by its name without the namespace it sits in.
Record the monomorphic structures and enumerations among `lean-clj.dsl` commands. Each is also known by its name without the namespace it sits in.
Structures and enumerations by Lean name:
{:kind :struct :fields [[field type] ...]} or {:kind :enum :ctors [ctor ...]}.
Structures and enumerations by Lean name:
`{:kind :struct :fields [[field type] ...]}` or `{:kind :enum :ctors [ctor ...]}`.(valid? t x)Whether x is a Clojure value of the Lean type t, telling lists from
vectors as the generated code does.
Whether `x` is a Clojure value of the Lean type `t`, telling lists from vectors as the generated code does.
(write-kondo-config! nss)Write kondo-config of nss to .clj-kondo/lean-clj/types/config.edn,
where clj-kondo picks it up.
Write `kondo-config` of `nss` to `.clj-kondo/lean-clj/types/config.edn`, where clj-kondo picks it up.
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 |