diff --git a/lean4-verso-xp/Main.lean b/lean4-verso-xp/Main.lean index be5e8ce..9e1bcd9 100644 --- a/lean4-verso-xp/Main.lean +++ b/lean4-verso-xp/Main.lean @@ -9,6 +9,7 @@ where config := { -- destination := "dist", extraFiles := [("static", "static")], + extraCss := ["/static/overrides.css"], -- extraCss := ["/static/colors.css", "/static/theme.css", "/static/print.css", "/static/fonts/source-serif/source-serif-text.css", "/static/fonts/source-code-pro/source-code-pro.css", "/static/katex/katex.min.css"], -- extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"], extraJs := ["/static/math.js"], diff --git a/lean4-verso-xp/VersoXp/Math.lean b/lean4-verso-xp/VersoXp/Math.lean index a9b1958..3a70432 100644 --- a/lean4-verso-xp/VersoXp/Math.lean +++ b/lean4-verso-xp/VersoXp/Math.lean @@ -7,8 +7,8 @@ open Lean.MessageSeverity -- #check Verso.Doc.MathMode open Verso Doc Elab in -@[code_block_expander latex] -def Manual.latex : CodeBlockExpander +@[code_block_expander math] +def Manual.math: CodeBlockExpander | _args, str => do return #[(← `(Doc.Block.para #[Doc.Inline.math Doc.MathMode.display s!"{$str}"]))] @@ -32,9 +32,9 @@ $$`E=mc^2` ❌ But no support for multiline math yet. -The following is a workaround inspired by [lecopivo/scientific-computing-lean](https://github.com/lecopivo/scientific-computing-lean/blob/ae7f1f6359465687136a9e75e0c83a1ef19525c2/ScientificComputingInLean/Meta/Latex.lean): +The following is a workaround inspired by [lecopivo/scientific-computing-lean](https://github.com/lecopivo/scientific-computing-lean/blob/ae7f1f6359465687136a9e75e0c83a1ef19525c2/ScientificComputingInLean/Meta/Latex.lean), and the syntax is the same as [one variant of GFM for math](https://docs.github.com/en/get-started/writing-on-github/working-with-advanced-formatting/writing-mathematical-expressions#writing-expressions-as-blocks): -```latex +```math f'(x) = \lim_{h → 0} \frac{f(x+h) - f(x)}{h} ``` diff --git a/lean4-verso-xp/static/overrides.css b/lean4-verso-xp/static/overrides.css new file mode 100644 index 0000000..0095584 --- /dev/null +++ b/lean4-verso-xp/static/overrides.css @@ -0,0 +1,3 @@ +.section-toc { + display: none; +}