remark-lean
v0.0.8
Published
remark plugin for syntax-highlighting Lean 4 code blocks via the Lean LSP
Readme
remark-lean
A remark plugin that provides Verso-like features.
Quick start
You need Lean installed, and a Lean project already initialized.
Then pass rootUri as the path to that project.
import { remark } from "remark";
import remarkHtml from "remark-html";
import remarkLean from "remark-lean";
const html = await remark()
.use(remarkLean, { rootUri: "file:///path/to/lean-project" })
.use(remarkHtml, { sanitize: false })
.process(markdown);Then, include the runtime in your page to activate hover behavior.
import { leanHydrate } from "remark-lean/runtime";
leanHydrate();Default styles are shipped in remark-lean/dist/lean.css.
See examples in examples.
