Clojure functions with Lean signatures.
(lean-clj.typed/defn insert-sorted [x Int xs (List Int)] (List Int) ...)
The function is an ordinary Clojure function. Its signature and body are
kept in the var's :lean/sig metadata, from which (clojure insert-sorted)
in a deflean block renders a Lean model of the function to prove things
about.
Clojure functions with Lean signatures.
(lean-clj.typed/defn insert-sorted [x Int xs (List Int)] (List Int)
...)
The function is an ordinary Clojure function. Its signature and body are
kept in the var's `:lean/sig` metadata, from which `(clojure insert-sorted)`
in a `deflean` block renders a Lean model of the function to prove things
about.(check v)(check v {:keys [num-tests seed] :or {num-tests 100}})Compare the lean-clj.typed/defn function v with its Lean model on
inputs generated from the signature, as clojure.test.check/quick-check.
A call where the Clojure function throws is outside what the model
describes and passes; a result that is not a value of the return type
fails.
Compare the `lean-clj.typed/defn` function `v` with its Lean model on inputs generated from the signature, as `clojure.test.check/quick-check`. A call where the Clojure function throws is outside what the model describes and passes; a result that is not a value of the return type fails.
(defn nm & more)Define a function with a Lean signature: [x T y U] R as in deflean.
(defn name docstring? [x T ...] R body)
:termination-by and :decreasing-by metadata on the name give Lean the
termination argument of a recursive function.
Define a function with a Lean signature: `[x T y U] R` as in `deflean`. (defn name docstring? [x T ...] R body) `:termination-by` and `:decreasing-by` metadata on the name give Lean the termination argument of a recursive function.
(loop bindings & body)clojure.core/loop whose bindings carry Lean types: [i T init ...].
:termination-by and :decreasing-by metadata on the vector give Lean the
termination argument.
`clojure.core/loop` whose bindings carry Lean types: `[i T init ...]`. `:termination-by` and `:decreasing-by` metadata on the vector give Lean the termination argument.
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 |