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 opts)Compare the lean-clj.typed/defn function v with its Lean model on
inputs generated from the signature, as clojure.test.check/quick-check,
arity by arity. 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. The result is that of the first arity that fails, or of the last.
Options: :num-tests (100), :seed, :gens, a map from parameter names
to generators that replace the ones of their types, :at, the types of the
type variables of a polymorphic function ({α Int}, Int for the ones it
leaves out), :big-ints?, to generate integers beyond Long (which
recursion on a Nat would take that many steps to finish), :max-size, the
largest size of generated collections (200), and :throws, :pass (the
default) or :fail to count a call that throws as a failure.
A failure carries :counterexample: the arity, the shrunk arguments, and the
values of the function and of the model on them.
Compare the `lean-clj.typed/defn` function `v` with its Lean model on
inputs generated from the signature, as `clojure.test.check/quick-check`,
arity by arity. 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. The result is that of the first arity that fails, or of the last.
Options: `:num-tests` (100), `:seed`, `:gens`, a map from parameter names
to generators that replace the ones of their types, `:at`, the types of the
type variables of a polymorphic function (`{α Int}`, `Int` for the ones it
leaves out), `:big-ints?`, to generate integers beyond `Long` (which
recursion on a `Nat` would take that many steps to finish), `:max-size`, the
largest size of generated collections (200), and `:throws`, `:pass` (the
default) or `:fail` to count a call that throws as a failure.
A failure carries `:counterexample`: the arity, the shrunk arguments, and the
values of the function and of the model on them.(defcheck name f)(defcheck name f opts)A clojure.test test that runs check on the lean-clj.typed/defn
function f and reports the counterexample of a failure.
(defcheck sort-ints-agrees sort-ints {:num-tests 200})
A `clojure.test` test that runs `check` on the `lean-clj.typed/defn`
function `f` and reports the counterexample of a failure.
(defcheck sort-ints-agrees sort-ints {:num-tests 200})(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) (defn name docstring? ([x T] R body) ([x T y U] R body) ...)
Binders take (implicit α Type) and (inst (BEq α)) for a polymorphic
function, and & xs (List T) last for the rest arguments.
: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) (defn name docstring? ([x T] R body) ([x T y U] R body) ...) Binders take `(implicit α Type)` and `(inst (BEq α))` for a polymorphic function, and `& xs (List T)` last for the rest arguments. `:termination-by` and `:decreasing-by` metadata on the name give Lean the termination argument of a recursive function.
(letfn fns & body)clojure.core/letfn whose functions carry Lean signatures:
[(f [x T ...] R body) ...]. A function may call the ones before it, and
itself through recur or by name.
`clojure.core/letfn` whose functions carry Lean signatures: `[(f [x T ...] R body) ...]`. A function may call the ones before it, and itself through `recur` or by name.
(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 |