Skip to content

Commit

Permalink
Replace lt and gt with symbols
Browse files Browse the repository at this point in the history
  • Loading branch information
@ericluap
ericluap committed Aug 22, 2024
1 parent f0c77de commit 454812b
Show file tree
Hide file tree
Showing 6 changed files with 31 additions and 8 deletions.
24 changes: 24 additions & 0 deletions blueprint/print/print.fdb_latexmk
View file
Original file line number Diff line number Diff line change
@@ -1 +1,25 @@
# Fdb version 4
["pdflatex"] 1724299427 "print.tex" "/Users/eric/Documents/ordered_semigroups/blueprint/print/print.pdf" "print" 1724299437 2
"/Users/eric/Documents/ordered_semigroups/blueprint/print/mathtools.sty" 0 -1 0 ""
"/Users/eric/Documents/ordered_semigroups/blueprint/print/print.aux" 1722321103 32 3985256e7290058c681f74d7a3565a19 "pdflatex"
"/Users/eric/Library/TinyTeX/texmf-dist/tex/generic/iftex/iftex.sty" 1644112042 7237 bdd120a32c8fdb4b433cf9ca2e7cd98a ""
"/Users/eric/Library/TinyTeX/texmf-dist/tex/generic/iftex/ifvtex.sty" 1572645307 1057 525c2192b5febbd8c1f662c9468335bb ""
"/Users/eric/Library/TinyTeX/texmf-dist/tex/latex/amscls/amsthm.sty" 1591045760 12594 0d51ac3a545aaaa555021326ff22a6cc ""
"/Users/eric/Library/TinyTeX/texmf-dist/tex/latex/amsfonts/amsfonts.sty" 1359763108 5949 3f3fd50a8cc94c3d4cbf4fc66cd3df1c ""
"/Users/eric/Library/TinyTeX/texmf-dist/tex/latex/amsfonts/amssymb.sty" 1359763108 13829 94730e64147574077f8ecfea9bb69af4 ""
"/Users/eric/Library/TinyTeX/texmf-dist/tex/latex/base/report.cls" 1686341992 23203 eb8fb57cc7a1166aa455e38e2f887972 ""
"/Users/eric/Library/TinyTeX/texmf-dist/tex/latex/base/size10.clo" 1686341992 8448 74078c4a887f2cdcd57c3ec111622740 ""
"/Users/eric/Library/TinyTeX/texmf-dist/tex/latex/geometry/geometry.sty" 1578002852 41601 9cf6c5257b1bc7af01a58859749dd37a ""
"/Users/eric/Library/TinyTeX/texmf-dist/tex/latex/graphics/keyval.sty" 1654720880 2671 7e67d78d9b88c845599a85b2d41f2e39 ""
"/Users/eric/Library/TinyTeX/texmf-dist/tex/latex/l3backend/l3backend-xetex.def" 1681935207 31866 ab7ff58e8b7eb91f5882424abf292263 ""
"/Users/eric/Library/TinyTeX/texmf-dist/tex/latex/l3kernel/expl3.sty" 1691788416 6547 0a941b039a849be5d35eb6686a945e7a ""
"/Users/eric/Library/TinyTeX/texmf-dist/web2c/texmf.cnf" 1681165822 40967 d940221f8762fd5848760382d97d1226 ""
"/Users/eric/Library/TinyTeX/texmf-var/web2c/xetex/xelatex.fmt" 1692155742 9009158 40d0952685467d3eb55273d0f193ab0c ""
"/Users/eric/Library/TinyTeX/texmf.cnf" 1692222263 708 85fd07691b6294ba94c59dbc62380410 ""
"mathtools.sty" 0 -1 0 ""
"print.tex" 1722315696 1111 34db4771c46b4138f6190a5df05e8f82 ""
(generated)
"/Users/eric/Documents/ordered_semigroups/blueprint/print/print.aux"
"/Users/eric/Documents/ordered_semigroups/blueprint/print/print.log"
"/Users/eric/Documents/ordered_semigroups/blueprint/print/print.pdf"
(rewritten before read)
7 changes: 4 additions & 3 deletions blueprint/print/print.log
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
This is XeTeX, Version 3.141592653-2.6-0.999995 (TeX Live 2023) (preloaded format=xelatex 2023.8.16) 21 AUG 2024 18:36
This is XeTeX, Version 3.141592653-2.6-0.999995 (TeX Live 2023) (preloaded format=xelatex 2023.8.16) 21 AUG 2024 21:03
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
Expand Down Expand Up @@ -82,13 +82,14 @@ Package: amsthm 2020/05/29 v2.20.6
Type X to quit or <RETURN> to proceed,
or enter new name. (Default extension: sty)

Enter file name:
Enter file name: X

! Emergency stop.
<read *>

l.20 \usepackage
[unicode,colorlinks=true,linkcolor=blue,urlcolor=magenta, ci...
End of file on the terminal!
*** (cannot \read from terminal in nonstop modes)


Here is how much of TeX's memory you used:
Expand Down
5 changes: 2 additions & 3 deletions blueprint/src/content.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,14 +39,13 @@ \section{Content}

\begin{definition}\label{def:positive}\lean{is_positive}\leanok
\uses{def:OrderedSemigroup}
An element $a$ of an ordered semigroup $S$
is \textbf{positive} if for all $x\in S$, $a*x \gt x$.
An element $a$ of an ordered semigroup $S$ is \textbf{positive} if for all $x\in S$, $a*x > x$.
\end{definition}

\begin{definition}\label{def:negative}\lean{is_negative}\leanok
\uses{def:OrderedSemigroup}
An element $a$ of an ordered semigroup $S$
is \textbf{negative} if for all $x\in S$, $a*x \lt x$.
is \textbf{negative} if for all $x\in S$, $a*x < x$.
\end{definition}

\begin{definition}\label{def:one}\lean{is_one}\leanok
Expand Down
Binary file modified blueprint/src/web.paux
View file
Binary file not shown.
2 changes: 1 addition & 1 deletion blueprint/web/dep_graph_document.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -629,7 +629,7 @@ <h1 id="doc_title">Dependencies</h1>
.width(width)
.height(height)
.fit(true)
.renderDot(`strict digraph "" { graph [bgcolor=transparent]; node [label="\N", penwidth=1.8 ]; edge [arrowhead=vee]; "lem:right_forall" [color=green, label=right_forall, shape=ellipse]; "thm:pos_neg_or_one" [color=green, fillcolor="#A3D6FF", label=pos_neg_or_one, shape=ellipse, style=filled]; "def:OrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedSemigroup, shape=box, style=filled]; "def:OrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:OrderedCancelSemigroup" [style=dashed]; "def:LinearOrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:LinearOrderedSemigroup" [style=dashed]; "def:positive" [color=green, fillcolor="#B0ECA3", label=positive, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:positive" [style=dashed]; "def:negative" [color=green, fillcolor="#B0ECA3", label=negative, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:negative" [style=dashed]; "def:one" [color=green, fillcolor="#B0ECA3", label=one, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:one" [style=dashed]; "def:LinearOrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedCancelSemigroup" -> "def:LinearOrderedCancelSemigroup" [style=dashed]; "def:positive" -> "lem:right_forall" [style=dashed]; "def:positive" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch_wrt" [color=green, fillcolor="#B0ECA3", label=arch_wrt, shape=box, style=filled]; "def:positive" -> "def:arch_wrt" [style=dashed]; "thm:neg_lt_pos" [color=green, fillcolor="#A3D6FF", label=neg_lt_pos, shape=ellipse, style=filled]; "def:positive" -> "thm:neg_lt_pos" [style=dashed]; "def:negative" -> "lem:right_forall" [style=dashed]; "def:negative" -> "thm:pos_neg_or_one" [style=dashed]; "def:negative" -> "def:arch_wrt" [style=dashed]; "def:negative" -> "thm:neg_lt_pos" [style=dashed]; "def:one" -> "lem:right_forall" [style=dashed]; "def:one" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch" [color=green, fillcolor="#B0ECA3", label=arch, shape=box, style=filled]; "def:one" -> "def:arch" [style=dashed]; "def:LinearOrderedCancelSemigroup" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch_wrt" -> "def:arch" [style=dashed]; non_arch_anomalous [color=green, fillcolor="#A3D6FF", label=non_arch_anomalous, shape=ellipse, style=filled]; "def:arch" -> non_arch_anomalous [style=dashed]; "def:anomalous_pair" [color=green, fillcolor="#B0ECA3", label=anomalous_pair, shape=box, style=filled]; "def:anomalous_pair" -> non_arch_anomalous [style=dashed]; "thm:comm_ineq" [color=green, fillcolor="#A3D6FF", label=comm_ineq, shape=ellipse, style=filled]; split_first_and_last [color=green, fillcolor="#A3D6FF", label=split_first_and_last, shape=ellipse, style=filled]; a0000000014 [color=blue, fillcolor="#A3D6FF", label=a0000000014, shape=ellipse, style=filled];}`)
.renderDot(`strict digraph "" { graph [bgcolor=transparent]; node [label="\N", penwidth=1.8 ]; edge [arrowhead=vee]; "thm:neg_lt_pos" [color=green, fillcolor="#A3D6FF", label=neg_lt_pos, shape=ellipse, style=filled]; "lem:right_forall" [color=green, label=right_forall, shape=ellipse]; non_arch_anomalous [color=green, fillcolor="#A3D6FF", label=non_arch_anomalous, shape=ellipse, style=filled]; "def:OrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedSemigroup, shape=box, style=filled]; "def:positive" [color=green, fillcolor="#B0ECA3", label=positive, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:positive" [style=dashed]; "def:OrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:OrderedCancelSemigroup" [style=dashed]; "def:LinearOrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:LinearOrderedSemigroup" [style=dashed]; "def:negative" [color=green, fillcolor="#B0ECA3", label=negative, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:negative" [style=dashed]; "def:one" [color=green, fillcolor="#B0ECA3", label=one, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:one" [style=dashed]; "def:positive" -> "thm:neg_lt_pos" [style=dashed]; "def:positive" -> "lem:right_forall" [style=dashed]; "def:arch_wrt" [color=green, fillcolor="#B0ECA3", label=arch_wrt, shape=box, style=filled]; "def:positive" -> "def:arch_wrt" [style=dashed]; "thm:pos_neg_or_one" [color=green, fillcolor="#A3D6FF", label=pos_neg_or_one, shape=ellipse, style=filled]; "def:positive" -> "thm:pos_neg_or_one" [style=dashed]; "def:LinearOrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedCancelSemigroup" -> "def:LinearOrderedCancelSemigroup" [style=dashed]; "def:negative" -> "thm:neg_lt_pos" [style=dashed]; "def:negative" -> "lem:right_forall" [style=dashed]; "def:negative" -> "def:arch_wrt" [style=dashed]; "def:negative" -> "thm:pos_neg_or_one" [style=dashed]; "def:one" -> "lem:right_forall" [style=dashed]; "def:one" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch" [color=green, fillcolor="#B0ECA3", label=arch, shape=box, style=filled]; "def:one" -> "def:arch" [style=dashed]; "def:arch_wrt" -> "def:arch" [style=dashed]; "def:LinearOrderedCancelSemigroup" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch" -> non_arch_anomalous [style=dashed]; "def:anomalous_pair" [color=green, fillcolor="#B0ECA3", label=anomalous_pair, shape=box, style=filled]; "def:anomalous_pair" -> non_arch_anomalous [style=dashed]; split_first_and_last [color=green, fillcolor="#A3D6FF", label=split_first_and_last, shape=ellipse, style=filled]; a0000000014 [color=blue, fillcolor="#A3D6FF", label=a0000000014, shape=ellipse, style=filled]; "thm:comm_ineq" [color=green, fillcolor="#A3D6FF", label=comm_ineq, shape=ellipse, style=filled];}`)
.on("end", interactive);

latexLabelEscaper = function(label) {
Expand Down
1 change: 0 additions & 1 deletion blueprint/web/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,6 @@ <h1>Lean declarations</h1>

</div>
</div>

<div class="definition_thmwrapper theorem-style-definition" id="def:LinearOrderedSemigroup">
<div class="definition_thmheading">
<span class="definition_thmcaption">
Expand Down

0 comments on commit 454812b

Please sign in to comment.