diff --git a/assets/latex.xsl b/assets/latex.xsl index f3ae292..95bf496 100644 --- a/assets/latex.xsl +++ b/assets/latex.xsl @@ -2,6 +2,7 @@ @@ -221,5 +222,13 @@ } } + + + \begin{lstlisting}[mathescape=true,language= + + ] + + \end{lstlisting} + \ No newline at end of file diff --git a/assets/shiki.js b/assets/shiki.js new file mode 100644 index 0000000..ea4ec48 --- /dev/null +++ b/assets/shiki.js @@ -0,0 +1,44 @@ +import { getHighlighter } from 'https://esm.sh/shiki@1.6.0' + +document.addEventListener('DOMContentLoaded', async () => { + + const lean4res = await fetch('https://cdn.jsdelivr.net/gh/leanprover/vscode-lean4@master/vscode-lean4/syntaxes/lean4.json') + + console.log(lean4res) + + if(!lean4res.ok) { + console.error('Failed to fetch lean4.json') + } + let lean4json; + try { + lean4json = await lean4res.json() + } catch(err) { + console.error(err); + } + + const codes = document.querySelectorAll('code') + codes.forEach(async code => { + let lang = code.getAttribute('class') || 'plaintext' + let langAlias = {} + + if((lang == 'lean4' || lang == 'lean') && lean4json) { + lang = lean4json + langAlias = { + lean4: 'Lean 4', + lean: 'Lean 4' + } + } + + const highlighter = await getHighlighter({ + langs: [lang], + langAlias, + themes: ['one-dark-pro'], + }) + + const html = await highlighter.codeToHtml( + code.textContent.replaceAll(/^\n/g, '').replaceAll(/\n$/g, ''), + { lang, theme: 'one-dark-pro' } + ) + code.innerHTML = html + }) +}) \ No newline at end of file diff --git a/assets/uts-layout.xsl b/assets/uts-layout.xsl index 21f3b33..c8ae868 100644 --- a/assets/uts-layout.xsl +++ b/assets/uts-layout.xsl @@ -30,6 +30,8 @@ + diff --git a/trees/ca-0001.tree b/trees/ca-0001.tree index 0877d0e..0fa7d13 100644 --- a/trees/ca-0001.tree +++ b/trees/ca-0001.tree @@ -65,4 +65,8 @@ } } } +} + +\block{Scracthpad}{ + \transclude{math-0001} } \ No newline at end of file diff --git a/trees/code.tex b/trees/code.tex new file mode 100644 index 0000000..1403886 --- /dev/null +++ b/trees/code.tex @@ -0,0 +1,13 @@ +\usepackage{listings} + +% handle Lean code highlighting following https://lean-lang.org/lean4/doc/syntax_highlight_in_latex.html +\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1} % red +\definecolor{tacticcolor}{rgb}{0.0, 0.1, 0.6} % blue +\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4} % grey +\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6} % blue +\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1} % green +\definecolor{attributecolor}{rgb}{0.7, 0.1, 0.1} % red + +\def\lstlanguagefiles{../trees/lstlean.tex} +% set default language +\lstset{language=lean} \ No newline at end of file diff --git a/trees/lstlean.tex b/trees/lstlean.tex new file mode 100644 index 0000000..2403bba --- /dev/null +++ b/trees/lstlean.tex @@ -0,0 +1,289 @@ +% Listing style definition for the Lean Theorem Prover. +% Defined by Jeremy Avigad, 2015, by modifying Assia Mahboubi's SSR style. +% Unicode replacements taken from Olivier Verdier's unixode.sty + +\lstdefinelanguage{lean} { + +% Anything between $ becomes LaTeX math mode +mathescape=false, +% Comments may or not include Latex commands +texcl=false, + +% keywords, list taken from lean-syntax.el +morekeywords=[1]{ +import, prelude, protected, private, noncomputable, definition, meta, renaming, +hiding, parameter, parameters, begin, constant, constants, +lemma, variable, variables, theory, +print, theorem, example, +open, as, export, override, axiom, axioms, inductive, with, +structure, record, universe, universes, +alias, help, precedence, reserve, declare_trace, add_key_equivalence, +match, infix, infixl, infixr, notation, postfix, prefix, instance, +eval, reduce, check, end, this, +using, using_well_founded, namespace, section, +attribute, local, set_option, extends, include, omit, class, +raw, replacing, +calc, have, show, suffices, by, in, at, let, forall, Pi, fun, +exists, if, dif, then, else, assume, obtain, from, register_simp_ext, unless, break, continue, +mutual, do, def, run_cmd, const, +partial, mut, where, macro, syntax, deriving, +return, try, catch, for, macro_rules, declare_syntax_cat, abbrev}, + +% Sorts +morekeywords=[2]{Sort, Type, Prop}, + +% tactics, list taken from lean-syntax.el +morekeywords=[3]{ +assumption, +apply, intro, intros, allGoals, +generalize, clear, revert, done, exact, +refine, repeat, cases, rewrite, rw, +simp, simp_all, contradiction, +constructor, injection, +induction, +}, + +% modifiers, taken from lean-syntax.el +% note: 'otherkeywords' is needed because these use a different symbol. +% this command doesn't allow us to specify a number -- they are put with [1] +% otherkeywords={ +% [persistent], [notation], [visible], [instance], [trans_instance], +% [class], [parsing-only], [coercion], [unfold_full], [constructor], +% [reducible], [irreducible], [semireducible], [quasireducible], [wf], +% [whnf], [multiple_instances], [none], [decl], [declaration], +% [relation], [symm], [subst], [refl], [trans], [simp], [congr], [unify], +% [backward], [forward], [no_pattern], [begin_end], [tactic], [abbreviation], +% [reducible], [unfold], [alias], [eqv], [intro], [intro!], [elim], [grinder], +% [localrefinfo], [recursor] +% }, + +% Various symbols +literate= +{α}{{\ensuremath{\mathrm{\alpha}}}}1 +{β}{{\ensuremath{\mathrm{\beta}}}}1 +{γ}{{\ensuremath{\mathrm{\gamma}}}}1 +{δ}{{\ensuremath{\mathrm{\delta}}}}1 +{ε}{{\ensuremath{\mathrm{\varepsilon}}}}1 +{ζ}{{\ensuremath{\mathrm{\zeta}}}}1 +{η}{{\ensuremath{\mathrm{\eta}}}}1 +{θ}{{\ensuremath{\mathrm{\theta}}}}1 +{ι}{{\ensuremath{\mathrm{\iota}}}}1 +{κ}{{\ensuremath{\mathrm{\kappa}}}}1 +{μ}{{\ensuremath{\mathrm{\mu}}}}1 +{ν}{{\ensuremath{\mathrm{\nu}}}}1 +{ξ}{{\ensuremath{\mathrm{\xi}}}}1 +{π}{{\ensuremath{\mathrm{\mathnormal{\pi}}}}}1 +{ρ}{{\ensuremath{\mathrm{\rho}}}}1 +{σ}{{\ensuremath{\mathrm{\sigma}}}}1 +{τ}{{\ensuremath{\mathrm{\tau}}}}1 +{φ}{{\ensuremath{\mathrm{\varphi}}}}1 +{χ}{{\ensuremath{\mathrm{\chi}}}}1 +{ψ}{{\ensuremath{\mathrm{\psi}}}}1 +{ω}{{\ensuremath{\mathrm{\omega}}}}1 + +{Γ}{{\ensuremath{\mathrm{\Gamma}}}}1 +{Δ}{{\ensuremath{\mathrm{\Delta}}}}1 +{Θ}{{\ensuremath{\mathrm{\Theta}}}}1 +{Λ}{{\ensuremath{\mathrm{\Lambda}}}}1 +{Σ}{{\ensuremath{\mathrm{\Sigma}}}}1 +{Φ}{{\ensuremath{\mathrm{\Phi}}}}1 +{Ξ}{{\ensuremath{\mathrm{\Xi}}}}1 +{Ψ}{{\ensuremath{\mathrm{\Psi}}}}1 +{Ω}{{\ensuremath{\mathrm{\Omega}}}}1 + +{ℵ}{{\ensuremath{\aleph}}}1 + +{≤}{{\ensuremath{\leq}}}1 +{≥}{{\ensuremath{\geq}}}1 +{≠}{{\ensuremath{\neq}}}1 +{≈}{{\ensuremath{\approx}}}1 +{≡}{{\ensuremath{\equiv}}}1 +{≃}{{\ensuremath{\simeq}}}1 + +{≤}{{\ensuremath{\leq}}}1 +{≥}{{\ensuremath{\geq}}}1 + +{∂}{{\ensuremath{\partial}}}1 +{∆}{{\ensuremath{\triangle}}}1 % or \laplace? + +{∫}{{\ensuremath{\int}}}1 +{∑}{{\ensuremath{\mathrm{\Sigma}}}}1 +{Π}{{\ensuremath{\mathrm{\Pi}}}}1 + +{⊥}{{\ensuremath{\perp}}}1 +{∞}{{\ensuremath{\infty}}}1 +{∂}{{\ensuremath{\partial}}}1 + +{∓}{{\ensuremath{\mp}}}1 +{±}{{\ensuremath{\pm}}}1 +{×}{{\ensuremath{\times}}}1 + +{⊕}{{\ensuremath{\oplus}}}1 +{⊗}{{\ensuremath{\otimes}}}1 +{⊞}{{\ensuremath{\boxplus}}}1 + +{∇}{{\ensuremath{\nabla}}}1 +{√}{{\ensuremath{\sqrt}}}1 + +{⬝}{{\ensuremath{\cdot}}}1 +{•}{{\ensuremath{\cdot}}}1 +{∘}{{\ensuremath{\circ}}}1 + +%{⁻}{{\ensuremath{^{\textup{\kern1pt\rule{2pt}{0.3pt}\kern-1pt}}}}}1 +{⁻}{{\ensuremath{^{-}}}}1 +{▸}{{\ensuremath{\blacktriangleright}}}1 + +{∧}{{\ensuremath{\wedge}}}1 +{∨}{{\ensuremath{\vee}}}1 +{¬}{{\ensuremath{\neg}}}1 +{⊢}{{\ensuremath{\vdash}}}1 + +%{⟨}{{\ensuremath{\left\langle}}}1 +%{⟩}{{\ensuremath{\right\rangle}}}1 +{⟨}{{\ensuremath{\langle}}}1 +{⟩}{{\ensuremath{\rangle}}}1 + +{↦}{{\ensuremath{\mapsto}}}1 +{←}{{\ensuremath{\leftarrow}}}1 +{<-}{{\ensuremath{\leftarrow}}}1 +{→}{{\ensuremath{\rightarrow}}}1 +{↔}{{\ensuremath{\leftrightarrow}}}1 +{⇒}{{\ensuremath{\Rightarrow}}}1 +{⟹}{{\ensuremath{\Longrightarrow}}}1 +{⇐}{{\ensuremath{\Leftarrow}}}1 +{⟸}{{\ensuremath{\Longleftarrow}}}1 + +{∩}{{\ensuremath{\cap}}}1 +{∪}{{\ensuremath{\cup}}}1 +{⊂}{{\ensuremath{\subseteq}}}1 +{⊆}{{\ensuremath{\subseteq}}}1 +{⊄}{{\ensuremath{\nsubseteq}}}1 +{⊈}{{\ensuremath{\nsubseteq}}}1 +{⊃}{{\ensuremath{\supseteq}}}1 +{⊇}{{\ensuremath{\supseteq}}}1 +{⊅}{{\ensuremath{\nsupseteq}}}1 +{⊉}{{\ensuremath{\nsupseteq}}}1 +{∈}{{\ensuremath{\in}}}1 +{∉}{{\ensuremath{\notin}}}1 +{∋}{{\ensuremath{\ni}}}1 +{∌}{{\ensuremath{\notni}}}1 +{∅}{{\ensuremath{\emptyset}}}1 + +{∖}{{\ensuremath{\setminus}}}1 +{†}{{\ensuremath{\dag}}}1 + +{ℕ}{{\ensuremath{\mathbb{N}}}}1 +{ℤ}{{\ensuremath{\mathbb{Z}}}}1 +{ℝ}{{\ensuremath{\mathbb{R}}}}1 +{ℚ}{{\ensuremath{\mathbb{Q}}}}1 +{ℂ}{{\ensuremath{\mathbb{C}}}}1 +{⌞}{{\ensuremath{\llcorner}}}1 +{⌟}{{\ensuremath{\lrcorner}}}1 +{⦃}{{\ensuremath{\{\!|}}}1 +{⦄}{{\ensuremath{|\!\}}}}1 + +{‖}{{\ensuremath{\|}}}1 +{₁}{{\ensuremath{_1}}}1 +{₂}{{\ensuremath{_2}}}1 +{₃}{{\ensuremath{_3}}}1 +{₄}{{\ensuremath{_4}}}1 +{₅}{{\ensuremath{_5}}}1 +{₆}{{\ensuremath{_6}}}1 +{₇}{{\ensuremath{_7}}}1 +{₈}{{\ensuremath{_8}}}1 +{₉}{{\ensuremath{_9}}}1 +{₀}{{\ensuremath{_0}}}1 +{ᵢ}{{\ensuremath{_i}}}1 +{ⱼ}{{\ensuremath{_j}}}1 +{ₐ}{{\ensuremath{_a}}}1 + +{¹}{{\ensuremath{^1}}}1 + +{ₙ}{{\ensuremath{_n}}}1 +{ₘ}{{\ensuremath{_m}}}1 +{ₚ}{{\ensuremath{_p}}}1 +{↑}{{\ensuremath{\uparrow}}}1 +{↓}{{\ensuremath{\downarrow}}}1 + +{...}{{\ensuremath{\ldots}}}1 +{·}{{\ensuremath{\cdot}}}1 + +{▸}{{\ensuremath{\triangleright}}}1 + +{Σ}{{\color{symbolcolor}\ensuremath{\Sigma}}}1 +{Π}{{\color{symbolcolor}\ensuremath{\Pi}}}1 +{∀}{{\color{symbolcolor}\ensuremath{\forall}}}1 +{∃}{{\color{symbolcolor}\ensuremath{\exists}}}1 +{λ}{{\color{symbolcolor}\ensuremath{\mathrm{\lambda}}}}1 +{\$}{{\color{symbolcolor}\$}}1 + +{:=}{{\color{symbolcolor}:=}}1 +{=}{{\color{symbolcolor}=}}1 +{<|>}{{\color{symbolcolor}<|>}}1 +{<\$>}{{\color{symbolcolor}<\$>}}1 +{+}{{\color{symbolcolor}+}}1 +{*}{{\color{symbolcolor}*}}1, + +% Comments +%comment=[s][\itshape \color{commentcolor}]{/-}{-/}, +morecomment=[s][\color{commentcolor}]{/-}{-/}, +morecomment=[l][\itshape \color{commentcolor}]{--}, + +% Spaces are not displayed as a special character +showstringspaces=false, + +% keep spaces +keepspaces=true, + +% String delimiters +morestring=[b]", +morestring=[d]’, + +% Size of tabulations +tabsize=3, + +% Enables ASCII chars 128 to 255 +extendedchars=false, + +% Case sensitivity +sensitive=true, + +% Automatic breaking of long lines +breaklines=true, +breakatwhitespace=true, + +% Default style fors listingsred +basicstyle=\ttfamily\small, + +% Position of captions is bottom +captionpos=b, + +% Full flexible columns +columns=[l]fullflexible, + + +% Style for (listings') identifiers +identifierstyle={\ttfamily\color{black}}, +% Note : highlighting of Coq identifiers is done through a new +% delimiter definition through an lstset at the beginning of the +% document. Don't know how to do better. + +% Style for declaration keywords +keywordstyle=[1]{\ttfamily\color{keywordcolor}}, + +% Style for sorts +keywordstyle=[2]{\ttfamily\color{sortcolor}}, + +% Style for tactics keywords +keywordstyle=[3]{\ttfamily\color{tacticcolor}}, + +% Style for attributes +keywordstyle=[4]{\ttfamily\color{attributecolor}}, + +% Style for strings +stringstyle=\ttfamily, + +% Style for comments +commentstyle={\ttfamily\footnotesize }, + +} \ No newline at end of file diff --git a/trees/macros.tree b/trees/macros.tree index 9462ec5..603fb3e 100644 --- a/trees/macros.tree +++ b/trees/macros.tree @@ -138,22 +138,21 @@ } } -\p{\code{tikz[g]}: A TikZ graph rendered via LaTeX.} +\p{\code{tikz[a]}: A TikZ graph rendered via LaTeX.} -\def\tikz[g]{ - \xml{center}{\tex{ +\def\tikz[a]{ + \tex{ \usepackage{tikz-cd} \usepackage{amssymb} }{ - \g + \a } - } } \p{\code{codeblock[lang][body]}: A code block specifying the language.} \def\codeblock[lang][body]{ - \pre{ \xml{code}[class]{\lang}{\body} } + \[class]{\lang}{\body} } \strong{Useful macros we defined} diff --git a/trees/math-0001.tree b/trees/math-0001.tree index 6ff6534..5c774a7 100644 --- a/trees/math-0001.tree +++ b/trees/math-0001.tree @@ -21,5 +21,18 @@ where #{[P]} is defined as: } \p{In Lean 4, the Kronecker delta [could be defined as](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/kronecker.20symbol):} -\code{def δ (i j : I) : R := (Pi.single i 1 : _ → R) j} +\codeblock{lean}{ +def δ (i j : I) : R := (Pi.single i 1 : _ → R) j + +theorem test (p q : Prop) (hp : p) (hq : q): p ∧ q ↔ q ∧ p := by + apply Iff.intro + . intro h + apply And.intro + . exact hq + . exact hp + . intro h + apply And.intro + . exact hp + . exact hq +} } diff --git a/trees/preamble.tex b/trees/preamble.tex index 388d7a4..e078ad6 100644 --- a/trees/preamble.tex +++ b/trees/preamble.tex @@ -248,4 +248,6 @@ \newcommand\placeholder[1]{\texttt{#1}} \newcommand\optional[1]{{\color{Grey} #1}} -\newcommand\pre{\mathtt{pre}} \ No newline at end of file +\newcommand\pre{\mathtt{pre}} + +\input{../trees/code} \ No newline at end of file