Benchmarking and LaTeX experiments

Changes

2 changed files (+23/-0)

• Benchmark.lean (new)
  • @@ -0,0 +1,6 @@
    + import Mathlib + + -- This is how you benchmark stuff I think + #count_heartbeats in + example {a b : ℝ} (hab : a * b ≤ 0) (ha : a ≠ 0) (hb : b ≠ 0) : (0 < a ∧ b < 0) ∨ (a < 0 ∧ 0 < b) := by + grind [mul_nonpos_iff_neg_imp_nonneg.mp hab]
• LaTeX.lean (new)
  • @@ -0,0 +1,17 @@
    + import ProofWidgets.Component.HtmlDisplay + + open scoped ProofWidgets.Jsx + + -- KaTeX supports CD but Mathjax doesn't sad + open ProofWidgets in + #html <MarkdownDisplay contents={" + ## Hello, Markdown + We have **bold text**, _italic text_, `example : True := by trivial`, + and $3×19 = \\int\\limits_0^{57}1~dx$. + + $$\\begin{CD} + S @>j>> T\\ + @VVV @VV + I @= p + \\end{CD}$$ + "} />