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, and a part that mixes letters with characters
Lean identifiers do not take is written in «» (operators stay as they are).
Lean identifier of a symbol or keyword: each `.`-separated part with a `-` becomes lowerCamelCase, and a part that mixes letters with characters Lean identifiers do not take is written in `«»` (operators stay as they are).
(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 |