Render Lean source from Clojure data.
Commands, terms, and tactics are written as S-expressions:
(def double [n Nat] Nat (+ n n)) (theorem double_eq [n Nat] (= (double n) (* 2 n)) (by (unfold double) omega))
(lean "...") embeds Lean source verbatim wherever a command, term, or
tactic is expected.
Render Lean source from Clojure data.
Commands, terms, and tactics are written as S-expressions:
(def double [n Nat] Nat (+ n n))
(theorem double_eq [n Nat] (= (double n) (* 2 n))
(by (unfold double) omega))
`(lean "...")` embeds Lean source verbatim wherever a command, term, or
tactic is expected.(binders bs)Lean binders of a vector: [x T y U] → (x : T) (y : U); the lists
(implicit x T), (strict x T), and (inst C) make one binder each.
Lean binders of a vector: `[x T y U]` → `(x : T) (y : U)`; the lists `(implicit x T)`, `(strict x T)`, and `(inst C)` make one binder each.
(ident x)Lean identifier of a symbol or keyword: each .-separated part with a -
becomes lowerCamelCase.
Lean identifier of a symbol or keyword: each `.`-separated part with a `-` becomes lowerCamelCase.
(render cmds)Lean source of a sequence of commands.
Lean source of a sequence of commands.
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 |