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!`).
Whether gen mixes in integers beyond Long.
Whether `gen` mixes in integers beyond `Long`.
Among types of the same short name, the one whose module starts with this prefix (the deflean modules of one Clojure namespace).
Among types of the same short name, the one whose module starts with this prefix (the deflean modules of one Clojure namespace).
(binder-parts bs)The parts of a lean-clj.typed binder vector [x T ... & xs (List T)]:
:params, the [name type] pairs of the fixed parameters, :rest, the pair
after &, :type-params, the binder lists ((implicit α Type),
(inst (BEq α))) that are not Clojure parameters, :type-vars, the names
they bind, and :args, the Clojure argument vector.
The parts of a `lean-clj.typed` binder vector `[x T ... & xs (List T)]`: `:params`, the `[name type]` pairs of the fixed parameters, `:rest`, the pair after `&`, `:type-params`, the binder lists (`(implicit α Type)`, `(inst (BEq α))`) that are not Clojure parameters, `:type-vars`, the names they bind, and `:args`, the Clojure argument vector.
(fn-schema v)malli function schema of a lean-clj.typed/defn var, for
malli.core/=>: [:=> [:cat T ...] R], or [:function ...] of one per
arity. Type variables become :any.
malli function schema of a `lean-clj.typed/defn` var, for `malli.core/=>`: `[:=> [:cat T ...] R]`, or `[:function ...]` of one per arity. Type variables become `:any`.
(gen t)test.check generator of the Clojure values of the Lean type t. Integers
include values beyond Long while *big-ints* is true.
test.check generator of the Clojure values of the Lean type `t`. Integers include values beyond `Long` while `*big-ints*` is true.
(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.
(module-of t)Lean module that defines the structure or enumeration t, if registered.
Lean module that defines the structure or enumeration `t`, if registered.
(register-commands! module cmds)Record the monomorphic structures and enumerations among the
lean-clj.dsl commands of the Lean module module.
Record the monomorphic structures and enumerations among the `lean-clj.dsl` commands of the Lean module `module`.
Structures and enumerations by full Lean name:
{:kind :struct :module m :fields [[field type] ...]} or
{:kind :enum :module m :ctors [ctor ...]}.
Structures and enumerations by full Lean name:
`{:kind :struct :module m :fields [[field type] ...]}` or
`{:kind :enum :module m :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 |