-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathguide.html
52 lines (47 loc) · 71.1 KB
/
guide.html
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
<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8" />
<link rel="icon" href="./favicon.png" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<link href="./_app/immutable/assets/0.DMdiiSda.css" rel="stylesheet">
<link rel="modulepreload" href="./_app/immutable/entry/start.DLVkKwsa.js">
<link rel="modulepreload" href="./_app/immutable/chunks/entry.BKyWPsLt.js">
<link rel="modulepreload" href="./_app/immutable/chunks/scheduler.qM0r6k2o.js">
<link rel="modulepreload" href="./_app/immutable/chunks/index.BfnljH8l.js">
<link rel="modulepreload" href="./_app/immutable/entry/app.D25Z7hcn.js">
<link rel="modulepreload" href="./_app/immutable/chunks/preload-helper.BQ24v_F8.js">
<link rel="modulepreload" href="./_app/immutable/chunks/index.4TzQEUL_.js">
<link rel="modulepreload" href="./_app/immutable/nodes/0.wyYiQk4x.js">
<link rel="modulepreload" href="./_app/immutable/nodes/3.DnTWAp2C.js"><title>Chip – Guide</title><!-- HEAD_svelte-1yvou92_START --><meta name="description" content="Guide"><!-- HEAD_svelte-1yvou92_END --><!-- HEAD_svelte-bnfb8z_START --><link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css" integrity="sha384-AfEj0r4/OFrOo5t7NnNe46zW/tFgW6x/bCJG8FqQCEo3+Aro6EYUG4+cU+KJWu/X" crossorigin="anonymous"><!-- HEAD_svelte-bnfb8z_END -->
</head>
<body data-sveltekit-preload-data="hover">
<div style="display: contents"> <div class="grid min-h-screen grid-rows-[auto_1fr]"> <div class="bg-slate-800 py-10"><article class="prose prose-invert mx-auto"><h1 data-svelte-h="svelte-wdfdui">Guide</h1> <h2 data-svelte-h="svelte-a4cwet">Grammar</h2> <!-- HTML_TAG_START --><span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mtable rowspacing="0.25em" columnalign="right left" columnspacing="0em"><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mo stretchy="false">⟨</mo><mtext mathvariant="italic">bexpr</mtext><mo stretchy="false">⟩</mo><mo>:</mo><mo>:</mo><mo>=</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mo stretchy="false">⟨</mo><mtext mathvariant="italic">rel-op</mtext><mo stretchy="false">⟩</mo><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"true"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"false"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"!"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">bexpr</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"("</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">bexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">")"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">bexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"&"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">bexpr</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">bexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"|"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">bexpr</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mo stretchy="false">⟨</mo><mtext mathvariant="italic">rel-op</mtext><mo stretchy="false">⟩</mo><mo>:</mo><mo>:</mo><mo>=</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"<"</mtext><mtext> </mtext><mo>∣</mo><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">">"</mtext><mtext> </mtext><mo>∣</mo><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"<="</mtext><mtext> </mtext><mo>∣</mo><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">">="</mtext><mtext> </mtext><mo>∣</mo><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"="</mtext><mtext> </mtext><mo>∣</mo><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"!="</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mo stretchy="false">⟨</mo><mtext mathvariant="italic">var</mtext><mo stretchy="false">⟩</mo><mo>:</mo><mo>:</mo><mo>=</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">r"[_a-zA-Z][_a-zA-Z0-9]*"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mo stretchy="false">⟨</mo><mtext mathvariant="italic">command</mtext><mo stretchy="false">⟩</mo><mo>:</mo><mo>:</mo><mo>=</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate-block</mtext><msup><mo stretchy="false">⟩</mo><mo>∗</mo></msup><mo stretchy="false">⟨</mo><mtext mathvariant="italic">command-kind</mtext><mo stretchy="false">⟩</mo><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate-block</mtext><msup><mo stretchy="false">⟩</mo><mo>∗</mo></msup></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mo stretchy="false">⟨</mo><mtext mathvariant="italic">command-kind</mtext><mo stretchy="false">⟩</mo><mo>:</mo><mo>:</mo><mo>=</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">var</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">":="</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"skip"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"if"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">guard</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"fi"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"do"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate-inv</mtext><mo stretchy="false">⟩</mo><mo stretchy="false">⟨</mo><mtext mathvariant="italic">guard</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"od"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">command</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"[]"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">command</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mo stretchy="false">⟨</mo><mtext mathvariant="italic">guard</mtext><mo stretchy="false">⟩</mo><mo>:</mo><mo>:</mo><mo>=</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">bexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"->"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">command</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">guard</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"[]"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">guard</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate-block</mtext><mo stretchy="false">⟩</mo><mo>:</mo><mo>:</mo><mo>=</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"{"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"}"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate-inv</mtext><mo stretchy="false">⟩</mo><mo>:</mo><mo>:</mo><mo>=</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"["</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"]"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate</mtext><mo stretchy="false">⟩</mo><mo>:</mo><mo>:</mo><mo>=</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mo stretchy="false">⟨</mo><mtext mathvariant="italic">rel-op</mtext><mo stretchy="false">⟩</mo><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"true"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"false"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"!"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"("</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">")"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"&"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"|"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"==>"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">quantifier</mtext><mo stretchy="false">⟩</mo><mo stretchy="false">⟨</mo><mtext mathvariant="italic">var</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"::"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">predicate</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mo stretchy="false">⟨</mo><mtext mathvariant="italic">quantifier</mtext><mo stretchy="false">⟩</mo><mo>:</mo><mo>:</mo><mo>=</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"exists"</mtext><mtext> </mtext><mo>∣</mo><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"forall"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mo>:</mo><mo>:</mo><mo>=</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">int</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">var</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"-"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic"><aexpr></mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"("</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic"><aexpr></mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">")"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"*"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"/"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"+"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">"-"</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">function</mtext><mo stretchy="false">⟩</mo></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mo stretchy="false">⟨</mo><mtext mathvariant="italic">function</mtext><mo stretchy="false">⟩</mo><mo>:</mo><mo>:</mo><mo>=</mo></mrow></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"division"</mtext><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"("</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">","</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">")"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"min"</mtext><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"("</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">","</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">")"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"max"</mtext><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"("</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">","</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">")"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"fac"</mtext><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"("</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">")"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"fib"</mtext><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"("</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">")"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr><mtr><mtd><mstyle scriptlevel="0" displaystyle="true"><mo lspace="0em" rspace="0em">∣</mo></mstyle></mtd><mtd><mstyle scriptlevel="0" displaystyle="true"><mrow><mrow></mrow><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"exp"</mtext><mtext> </mtext><mtext> </mtext><mtext mathvariant="monospace">"("</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">","</mtext><mtext> </mtext><mo stretchy="false">⟨</mo><mtext mathvariant="italic">aexpr</mtext><mo stretchy="false">⟩</mo><mtext> </mtext><mtext mathvariant="monospace">")"</mtext><mtext> </mtext></mrow></mstyle></mtd></mtr></mtable><annotation encoding="application/x-tex">
\begin{aligned}
\langle \textit{bexpr} \rangle ::= & \;\langle \textit{aexpr} \rangle \langle \textit{rel-op} \rangle \langle \textit{aexpr} \rangle \\ \mid & \;\;\texttt{"true"}\; \\ \mid & \;\;\texttt{"false"}\; \\ \mid & \;\;\texttt{"!"}\; \langle \textit{bexpr} \rangle \\ \mid & \;\;\texttt{"("}\; \langle \textit{bexpr} \rangle \;\texttt{")"}\; \\ \mid & \;\langle \textit{bexpr} \rangle \;\texttt{"\&"}\; \langle \textit{bexpr} \rangle \\ \mid & \;\langle \textit{bexpr} \rangle \;\texttt{"|"}\; \langle \textit{bexpr} \rangle \\\langle \textit{rel-op} \rangle ::= & \;\;\texttt{"<"}\; \mid \;\;\texttt{">"}\; \mid \;\;\texttt{"<="}\; \mid \;\;\texttt{">="}\; \mid \;\;\texttt{"="}\; \mid \;\;\texttt{"!="}\; \\\langle \textit{var} \rangle ::= & \;\;\texttt{r"[\_a-zA-Z][\_a-zA-Z0-9]*"}\; \\\langle \textit{command} \rangle ::= & \;\langle \textit{predicate-block} \rangle ^* \langle \textit{command-kind} \rangle \langle \textit{predicate-block} \rangle ^* \\\langle \textit{command-kind} \rangle ::= & \;\langle \textit{var} \rangle \;\texttt{":="}\; \langle \textit{aexpr} \rangle \\ \mid & \;\;\texttt{"skip"}\; \\ \mid & \;\;\texttt{"if"}\; \langle \textit{guard} \rangle \;\texttt{"fi"}\; \\ \mid & \;\;\texttt{"do"}\; \langle \textit{predicate-inv} \rangle \langle \textit{guard} \rangle \;\texttt{"od"}\; \\ \mid & \;\langle \textit{command} \rangle \;\texttt{"[]"}\; \langle \textit{command} \rangle \\\langle \textit{guard} \rangle ::= & \;\langle \textit{bexpr} \rangle \;\texttt{"->"}\; \langle \textit{command} \rangle \\ \mid & \;\langle \textit{guard} \rangle \;\texttt{"[]"}\; \langle \textit{guard} \rangle \\\langle \textit{predicate-block} \rangle ::= & \;\;\texttt{"\{"}\; \langle \textit{predicate} \rangle \;\texttt{"\}"}\; \\\langle \textit{predicate-inv} \rangle ::= & \;\;\texttt{"["}\; \langle \textit{predicate} \rangle \;\texttt{"]"}\; \\\langle \textit{predicate} \rangle ::= & \;\langle \textit{aexpr} \rangle \langle \textit{rel-op} \rangle \langle \textit{aexpr} \rangle \\ \mid & \;\;\texttt{"true"}\; \\ \mid & \;\;\texttt{"false"}\; \\ \mid & \;\;\texttt{"!"}\; \langle \textit{predicate} \rangle \\ \mid & \;\;\texttt{"("}\; \langle \textit{predicate} \rangle \;\texttt{")"}\; \\ \mid & \;\langle \textit{predicate} \rangle \;\texttt{"\&"}\; \langle \textit{predicate} \rangle \\ \mid & \;\langle \textit{predicate} \rangle \;\texttt{"|"}\; \langle \textit{predicate} \rangle \\ \mid & \;\langle \textit{predicate} \rangle \;\texttt{"==>"}\; \langle \textit{predicate} \rangle \\ \mid & \;\langle \textit{quantifier} \rangle \langle \textit{var} \rangle \;\texttt{"::"}\; \langle \textit{predicate} \rangle \\\langle \textit{quantifier} \rangle ::= & \;\;\texttt{"exists"}\; \mid \;\;\texttt{"forall"}\; \\\langle \textit{aexpr} \rangle ::= & \;\langle \textit{int} \rangle \\ \mid & \;\langle \textit{var} \rangle \\ \mid & \;\;\texttt{"-"}\; \langle \textit{<aexpr>} \rangle \\ \mid & \;\;\texttt{"("}\; \langle \textit{<aexpr>} \rangle \;\texttt{")"}\; \\ \mid & \;\langle \textit{aexpr} \rangle \;\texttt{"*"}\; \langle \textit{aexpr} \rangle \\ \mid & \;\langle \textit{aexpr} \rangle \;\texttt{"/"}\; \langle \textit{aexpr} \rangle \\ \mid & \;\langle \textit{aexpr} \rangle \;\texttt{"+"}\; \langle \textit{aexpr} \rangle \\ \mid & \;\langle \textit{aexpr} \rangle \;\texttt{"-"}\; \langle \textit{aexpr} \rangle \\ \mid & \;\langle \textit{function} \rangle \\\langle \textit{function} \rangle ::= & \;\;\texttt{"division"}\; \;\texttt{"("}\; \langle \textit{aexpr} \rangle \;\texttt{","}\; \langle \textit{aexpr} \rangle \;\texttt{")"}\; \\ \mid & \;\;\texttt{"min"}\; \;\texttt{"("}\; \langle \textit{aexpr} \rangle \;\texttt{","}\; \langle \textit{aexpr} \rangle \;\texttt{")"}\; \\ \mid & \;\;\texttt{"max"}\; \;\texttt{"("}\; \langle \textit{aexpr} \rangle \;\texttt{","}\; \langle \textit{aexpr} \rangle \;\texttt{")"}\; \\ \mid & \;\;\texttt{"fac"}\; \;\texttt{"("}\; \langle \textit{aexpr} \rangle \;\texttt{")"}\; \\ \mid & \;\;\texttt{"fib"}\; \;\texttt{"("}\; \langle \textit{aexpr} \rangle \;\texttt{")"}\; \\ \mid & \;\;\texttt{"exp"}\; \;\texttt{"("}\; \langle \textit{aexpr} \rangle \;\texttt{","}\; \langle \textit{aexpr} \rangle \;\texttt{")"}\; \\
\end{aligned}
</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:66em;vertical-align:-32.75em;"></span><span class="mord"><span class="mtable"><span class="col-align-r"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:33.25em;"><span style="top:-35.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">bexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">::=</span></span></span><span style="top:-33.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-32.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-30.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-29.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-27.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-26.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-24.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">rel-op</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">::=</span></span></span><span style="top:-23.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">var</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">::=</span></span></span><span style="top:-21.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">command</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">::=</span></span></span><span style="top:-20.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">command-kind</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">::=</span></span></span><span style="top:-18.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-17.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-15.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-14.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-12.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">guard</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">::=</span></span></span><span style="top:-11.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-9.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate-block</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">::=</span></span></span><span style="top:-8.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate-inv</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">::=</span></span></span><span style="top:-6.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">::=</span></span></span><span style="top:-5.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-3.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-2.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:-0.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:0.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:2.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:3.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:5.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:6.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">quantifier</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">::=</span></span></span><span style="top:8.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">::=</span></span></span><span style="top:9.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:11.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:12.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:14.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:15.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:17.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:18.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:20.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:21.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">function</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">::=</span></span></span><span style="top:23.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:24.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:26.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:27.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span><span style="top:29.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mrel">∣</span></span></span></span><span class="vlist-s"></span></span><span class="vlist-r"><span class="vlist" style="height:32.75em;"><span></span></span></span></span></span><span class="col-align-l"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:33.25em;"><span style="top:-35.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">rel-op</span></span><span class="mclose">⟩</span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span></span></span><span style="top:-33.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"true"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:-32.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"false"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:-30.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"!"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">bexpr</span></span><span class="mclose">⟩</span></span></span><span style="top:-29.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"("</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">bexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">")"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:-27.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">bexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"&"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">bexpr</span></span><span class="mclose">⟩</span></span></span><span style="top:-26.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">bexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"|"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">bexpr</span></span><span class="mclose">⟩</span></span></span><span style="top:-24.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"<"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">∣</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">">"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">∣</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"<="</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">∣</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">">="</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">∣</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"="</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">∣</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"!="</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:-23.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">r"[_a-zA-Z][_a-zA-Z0-9]*"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:-21.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate-block</span></span><span class="mclose"><span class="mclose">⟩</span><span class="msupsub"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.7387em;"><span style="top:-3.113em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mbin mtight">∗</span></span></span></span></span></span></span></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">command-kind</span></span><span class="mclose">⟩</span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate-block</span></span><span class="mclose"><span class="mclose">⟩</span><span class="msupsub"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.7387em;"><span style="top:-3.113em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mbin mtight">∗</span></span></span></span></span></span></span></span></span></span><span style="top:-20.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">var</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">":="</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span></span></span><span style="top:-18.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"skip"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:-17.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"if"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">guard</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"fi"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:-15.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"do"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate-inv</span></span><span class="mclose">⟩</span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">guard</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"od"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:-14.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">command</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"[]"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">command</span></span><span class="mclose">⟩</span></span></span><span style="top:-12.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">bexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"->"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">command</span></span><span class="mclose">⟩</span></span></span><span style="top:-11.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">guard</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"[]"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">guard</span></span><span class="mclose">⟩</span></span></span><span style="top:-9.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"{"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"}"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:-8.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"["</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"]"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:-6.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">rel-op</span></span><span class="mclose">⟩</span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span></span></span><span style="top:-5.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"true"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:-3.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"false"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:-2.41em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"!"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate</span></span><span class="mclose">⟩</span></span></span><span style="top:-0.91em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"("</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">")"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:0.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"&"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate</span></span><span class="mclose">⟩</span></span></span><span style="top:2.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"|"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate</span></span><span class="mclose">⟩</span></span></span><span style="top:3.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"==>"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate</span></span><span class="mclose">⟩</span></span></span><span style="top:5.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">quantifier</span></span><span class="mclose">⟩</span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">var</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"::"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">predicate</span></span><span class="mclose">⟩</span></span></span><span style="top:6.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"exists"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">∣</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"forall"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:8.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">int</span></span><span class="mclose">⟩</span></span></span><span style="top:9.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">var</span></span><span class="mclose">⟩</span></span></span><span style="top:11.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"-"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit"><aexpr></span></span><span class="mclose">⟩</span></span></span><span style="top:12.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"("</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit"><aexpr></span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">")"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:14.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"*"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span></span></span><span style="top:15.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"/"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span></span></span><span style="top:17.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"+"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span></span></span><span style="top:18.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"-"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span></span></span><span style="top:20.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">function</span></span><span class="mclose">⟩</span></span></span><span style="top:21.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"division"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"("</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">","</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">")"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:23.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"min"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"("</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">","</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">")"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:24.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"max"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"("</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">","</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">")"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:26.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"fac"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"("</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">")"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:27.59em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"fib"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"("</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">")"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span><span style="top:29.09em;"><span class="pstrut" style="height:3em;"></span><span class="mord"><span class="mord"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"exp"</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">"("</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">","</span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mopen">⟨</span><span class="mord text"><span class="mord textit">aexpr</span></span><span class="mclose">⟩</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mord text"><span class="mord texttt">")"</span></span><span class="mspace" style="margin-right:0.2778em;"></span></span></span></span><span class="vlist-s"></span></span><span class="vlist-r"><span class="vlist" style="height:32.75em;"><span></span></span></span></span></span></span></span></span></span></span></span><!-- HTML_TAG_END --></article></div></div>
<script>
{
__sveltekit_14aeb6 = {
base: new URL(".", location).pathname.slice(0, -1)
};
const element = document.currentScript.parentElement;
const data = [null,null];
Promise.all([
import("./_app/immutable/entry/start.DLVkKwsa.js"),
import("./_app/immutable/entry/app.D25Z7hcn.js")
]).then(([kit, app]) => {
kit.start(app, element, {
node_ids: [0, 3],
data,
form: null,
error: null
});
});
}
</script>
</div>
<script src="/coi-serviceworker.js" is:inline></script>
</body>
</html>