model/common.typ at main · Trebor-Huang/model · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
#import "@preview/cetz:0.5.2": canvas, draw
#import "@preview/fletcher:0.5.8" as fletcher: diagram, node, edge
#let diagram = diagram.with(label-size: 0.85em, label-sep: 0.15em)
#let edgeL = edge.with(label-side: left)
#let edgeR = edge.with(label-side: right)
#let edgeM = edge.with(label-side: center)

#let hyperlink(dest, body) = link(dest, underline(text(fill: color.oklch(45%, 55%, 250deg), body), offset: 0.2em))
#let author-note(body) = [
  #set text(fill: luma(60%))
  #body
]
#let author-notes(body) = block(fill: luma(90%), radius: 0.5em, outset: 0.5em)[
  #body
]

// Translation (used for indexing)
#let translation-table = state("translations", ())
#let add-entry(zh, en, key) = translation-table.update(it => {
  let actual = key
  if actual == none {
    actual = en.at("text", default: "")
  }
  it.push((zh, en, actual))
  it
})
#let translate(zh, en, key:none) = [#zh #text(fill: luma(40%))[(#en)]#add-entry(zh,en,key)]
#let define(zh, en, key:none) = [*#zh* #text(fill: luma(40%))[(#en)]#add-entry(zh,en,key)]

// Defintions
#import "@preview/ctheorems:1.1.3": *  // todo replace
#let thmstyle = thmplain.with(
  separator: [*.* ],
  titlefmt: strong,
  namefmt: x => [(#x)],
  bodyfmt: content => content + parbreak(),
  inset: (left: 0em, right: 0em),
  base_level: 2
)

#let theorem = thmstyle("theorem", "定理")
#let lemma = thmstyle("theorem", "引理")
#let definition = thmstyle("theorem", "定义")
#let proof = thmproof(
  "proof", "证明",
  separator: h(0em),
  titlefmt: box.with(stroke: 0.5pt, outset: (top: 0.25em, bottom: 0.25em, left: 0.1em, right: 0.1em)),
  inset: (left: 0em, right: 0em),
)
// In appendices, we need to fix the numbering
#let theorem-appendix = theorem.with(numbering: "A.1")
#let lemma-appendix = lemma.with(numbering: "A.1")
#let definition-appendix = definition.with(numbering: "A.1")

// Figure
#let numbered-figure = figure.with(kind: "numbered-figure", supplement: "图表", numbering: "1", gap: 1em)

// Equations
#let eq(content, top: 0pt, bottom: 0pt) = [\
  #box(align(center, content), width: 1fr, inset: (top: top, bottom: bottom))\
] // TODO manually tune some vertical spacing

// Inference rules
#let rule(concl, ..prem) = if type(prem.at(0, default: none)) == array {
    math.frac(box(
      inset: (bottom: 0.25em),
      prem.pos()
      .map(it => math.equation(it.intersperse(math.quad).join()))
      .intersperse("\n").join()
    ),
      concl.intersperse(math.quad).join())
  } else {
    math.frac(prem.pos().intersperse(math.quad).join(),concl)
  }
#let partir(..rules) = for rule in rules.pos() {
  box(math.equation(rule, block: true), inset: (left: 1em, right: 1em))
}
// Other type theoretic stuff
#let istype = math.op(math.sans("type"))
#let isnf = math.op(text(fill: color.oklch(50%, 80%, 200deg), math.sans("nf")))
#let isne = math.op(text(fill: color.oklch(50%, 80%, 80deg), math.sans("ne")))
#let isvar = math.op(text(fill: color.oklch(50%, 0%, 0deg), math.sans("var")))
#let typeof = math.op("typeof")
#let interpret(x) = math.lr(math.class("opening",sym.bracket.stroked) + x + math.class("closing",sym.bracket.stroked.r))
#let bind = math.class("punctuation", ".")
#let Empty = math.bb("0")
#let Unit = math.bb("1")
#let Bool = math.bb("2")
#let ite(b,t,f) = $"if" #b "then" #t "else" #f$
#let refl = math.op(text("refl", font: "New Computer Modern"))
#let transp = math.op(text("transport", font: "New Computer Modern"))
#let contr = math.op(text("contr", font: "New Computer Modern"))
#let Set = math.sans("Set")
#let Psh = math.sans("Psh")
#let yo = math.class("unary", box("よ", inset: (left: -0.1em, right: -0.1em)))
#let cod = math.op("cod")
#let dom = math.op("dom")

#let xarrow(arrow: sym.arrow, ..args, sup: none, sub: none) = {
  if args.pos().len() >= 1 {
    sup = args.pos().at(0)
  }
  if args.pos().len() >= 2 {
    sub = args.pos().at(1)
  }
  context {
    let lsup = measure($script(sup)$)
    let lsub = measure($script(sub)$)
    math.attach(math.stretch(arrow, size: calc.max(lsup.width, lsub.width) + 0.75em), t: box($script(sup)$, inset: (bottom: -0.3em)), b: box($script(sub)$, inset: (top: -1.1em), baseline: 100%))
  }
}
#let corner = symbol(
  "⌜",
  ("ul", "⌜"),
  ("ur", "⌝"),
  ("ll", "⌞"),
  ("lr", "⌟"),
)
#let corner-dict = (
  "dr": corner.lr,
  "dl": corner.ll,
  "ul": corner.ul,
  "ur": corner.ur
)
#let pullback(n) = edgeM("dr", " ", corner-dict.at(n), label-pos: 0%, label-size: 1em)