Utensil's Zettelkasten-style forest of evergreen notes on math and tech.
utensil.tngl.sh/forest/
Initial implementation of `\lean{}`
+107
-3
+36
-1
assets/uts-overrides.xsl
+36
-1
assets/uts-overrides.xsl
···
27
27
</span>
28
28
</xsl:template> -->
29
29
30
+
<xsl:template name="splitlean">
31
+
<xsl:param name="pText" select="."/>
32
+
<xsl:param name="sep" select="."/>
33
+
<xsl:if test="string-length($pText)">
34
+
<xsl:if test="not($pText=.)">
35
+
<!-- <xsl:text>,</xsl:text> -->
36
+
</xsl:if>
37
+
<a target="_blank" href="https://leanprover-community.github.io/mathlib4_docs/find/#doc/{substring-before(concat($pText,$sep),$sep)}">
38
+
<!-- <xsl:text>L∃∀N</xsl:text> -->
39
+
<xsl:value-of select="substring-before(concat($pText,$sep),$sep)" />
40
+
</a>
41
+
<xsl:call-template name="splitlean">
42
+
<xsl:with-param name="pText" select="substring-after($pText, $sep)"/>
43
+
<xsl:with-param name="sep" select="$sep"/>
44
+
</xsl:call-template>
45
+
</xsl:if>
46
+
</xsl:template>
47
+
48
+
<xsl:template match="f:meta[@name='lean']">
49
+
<span class="meta-lean">
50
+
<div class="meta-lean-list">
51
+
<xsl:call-template name="splitlean">
52
+
<xsl:with-param name="pText" select="."/>
53
+
<xsl:with-param name="sep" select="','"/>
54
+
</xsl:call-template>
55
+
</div>
56
+
<!-- <span class="meta-lean-symbol">✓</span> -->
57
+
<span class="meta-lean-symbol">L∃∀N</span>
58
+
</span>
59
+
</xsl:template>
60
+
30
61
<!-- Override the addr template -->
31
62
<xsl:template match="f:addr" priority="10">
32
63
<a class="slug" href="{../f:route}">
···
60
91
</xsl:choose>
61
92
</xsl:if>
62
93
<!-- uts-end -->
94
+
<!-- uts-begin -->
95
+
<!-- match f:meta with attribute lean -->
96
+
<xsl:if test="../f:meta[@name='lean']">
97
+
<xsl:apply-templates select="../f:meta[@name='lean']" />
98
+
</xsl:if>
63
99
</xsl:template>
64
100
65
101
<!-- uts-begin: Override embeded-tex to be injected SVG to support dark theme, resize etc. -->
···
113
149
<xsl:apply-templates select="f:mainmatter" mode="toc" />
114
150
</li>
115
151
</xsl:template>
116
-
117
152
118
153
</xsl:stylesheet>
+68
assets/uts-style.css
+68
assets/uts-style.css
···
381
381
/* :root[data-applied-mode="dark"] nav#toc .link.local.active {
382
382
color: color-mix(in srgb, var(--uts-text) 30%, yellow 70%);
383
383
} */
384
+
385
+
386
+
/* a.slug {
387
+
word-break: keep-all;
388
+
} */
389
+
390
+
.meta-lean {
391
+
display: block;
392
+
float: right;
393
+
height: 2em;
394
+
width: 5%;
395
+
cursor: pointer;
396
+
position: relative;
397
+
z-index: 1;
398
+
}
399
+
400
+
/* clearfix hack */
401
+
/* header h1::after {
402
+
content: "";
403
+
clear: both;
404
+
display: table;
405
+
} */
406
+
407
+
.meta-lean a, .meta-lean-symbol {
408
+
font-weight: normal;
409
+
font-family: Fira Code, DejaVu Sans Mono, monospace;
410
+
font-size: 60%;
411
+
border-radius: 5px;
412
+
color: var(--uts-text-gentle) !important;
413
+
background-color: var(--uts-background) !important;
414
+
border: var(--uts-text-gentle) 1px solid;
415
+
padding: 3px 1ex 3px 1ex;
416
+
margin: 0 0.5ex 1ex 0.5ex;
417
+
cursor: pointer;
418
+
float: right;
419
+
}
420
+
421
+
/* details:hover > summary .meta-lean a {
422
+
display: inline;
423
+
} */
424
+
425
+
.meta-lean-symbol {
426
+
/* margin: 1ex 0.5ex 1ex 0.5ex; */
427
+
/* cursor: pointer; */
428
+
/* visibility: hidden; */
429
+
/* text-align: right; */
430
+
/* font-weight: normal;
431
+
font-family: Fira Code, DejaVu Sans Mono, monospace; */
432
+
}
433
+
434
+
.meta-lean-list {
435
+
display: none;
436
+
visibility: hidden;
437
+
}
438
+
439
+
.meta-lean:hover .meta-lean-list {
440
+
display: block;
441
+
visibility: visible;
442
+
}
443
+
444
+
.meta-lean-list:hover {
445
+
display: block;
446
+
visibility: visible;
447
+
}
448
+
449
+
.meta-lean:hover .meta-lean-symbol {
450
+
visibility: hidden;
451
+
}
+1
-1
trees/ca-0006.tree
+1
-1
trees/ca-0006.tree
···
14
14
15
15
\p{Let #{\rfun : R \rmap T(M)} be the canonical map from #{R} to #{T(M)}, as a ring homomorphism.}
16
16
17
-
\p{A \vocab{Clifford algebra} over #{Q}, denoted #{\Cl (Q)}, is
17
+
\p{A \newvocab{Clifford algebra} over #{Q}, denoted #{\Cl (Q)}, is
18
18
the \vocab{ring quotient} of the \vocab{tensor algebra} #{T(M)}
19
19
by the equivalence relation satisfying #{\iota(m)^2 \sim \rfun(Q(m))} for all #{m \in M}.}
20
20