r53

Author: OlingCat

next/common/css/term.css

@@ -0,0 +1,12 @@
+.term {
+  font-weight: bold;
+  display: inline-flex;
+  flex-direction: column-reverse;
+  align-items: center;
+  vertical-align: bottom;
+}
+.term-en {
+  font-size: 0.6em;
+  line-height: 0.5em;
+  text-wrap: nowrap;
+}

next/common/term.js

@@ -0,0 +1,34 @@
+const docs = document.querySelectorAll(".doc");
+const term = /【([^】]+?)\|(.+?)】/gu;
+const bold = /【(.+?)】/gu;
+
+// 添加术语样式
+docs.forEach((el) => {
+  let content = el.innerHTML;
+  content = content.replace(
+    term,
+    `<div class="term">
+  <div class="term-zh">$1</div>
+  <div class="term-en">$2</div>
+</div>`,
+  );
+  content = content.replace(bold, "<strong>$1</strong>");
+  el.innerHTML = content;
+});
+
+// 调整术语大小
+const terms = document.getElementsByClassName("term-zh");
+for (const term of terms) {
+  const len = term.innerText.length;
+  console.log(len);
+  term.parentElement.style.width = len + "em";
+}
+
+// 移除多余的空格
+const newline = /(?<=[，。、：；」）])\n(?!\n)/gu;
+// const space = /\s*(<.+?>\p{Script=Han}.*?<\/.+?>)\s*/gu;
+const paras = document.querySelectorAll(".doc");
+for (const p of paras) {
+  p.innerHTML = p.innerHTML.replace(newline, "");
+  // p.innerHTML = p.innerHTML.replace(space, "$1");
+}

next/lf-current/AltAuto.html

@@ -2410,7 +2410,7 @@ <h1 class="libtitle">AltAuto<span class="subtitle">A Streamlined Treatment of Au
 </div>
 <div class="code">
 
-<span class="comment">(*&nbsp;2026-02-27&nbsp;12:25&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2026-06-19&nbsp;17:02&nbsp;*)</span><br/>
 </div>
 </div>
 

next/lf-current/AltAuto.v

@@ -1825,4 +1825,4 @@ Definition manual_grade_for_nor_intuition : option (nat*string) := None.
 
     - Ltac functions and [match goal] *)
 
-(* 2026-02-27 12:25 *)
+(* 2026-06-19 17:02 *)

next/lf-current/AltAutoTest.v

@@ -269,4 +269,4 @@ idtac "---------- nor_intuition ---------".
 idtac "MANUAL".
 Abort.
 
-(* 2026-02-27 12:26 *)
+(* 2026-06-19 17:02 *)

next/lf-current/Auto.html

@@ -906,7 +906,7 @@ <h1 class="libtitle">Auto<span class="subtitle">More Automation</span></h1>
 <span class="id" title="keyword">Proof</span>.<br/>
 &nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> <span class="id" title="var">HP</span> <span class="id" title="var">HQ</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">HP</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">y</span> <span class="id" title="var">HP'</span>]. <span class="id" title="tactic">eauto</span>.<br/>
 <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
-<span class="comment">(*&nbsp;2026-02-27&nbsp;12:25&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2026-06-19&nbsp;17:02&nbsp;*)</span><br/>
 </div>
 </div>
 

next/lf-current/Auto.v

@@ -744,4 +744,4 @@ Proof.
   intros P Q HP HQ. destruct HP as [y HP']. eauto.
 Qed.
 
-(* 2026-02-27 12:25 *)
+(* 2026-06-19 17:02 *)

next/lf-current/AutoTest.v

@@ -63,4 +63,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2026-02-27 12:26 *)
+(* 2026-06-19 17:02 *)

next/lf-current/Basics.html

@@ -2736,7 +2736,7 @@ <h1 class="libtitle">Basics<span class="subtitle">Functional Programming in Rocq
 </div>
 <div class="code">
 
-<span class="comment">(*&nbsp;2026-02-27&nbsp;12:25&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2026-06-19&nbsp;17:02&nbsp;*)</span><br/>
 </div>
 </div>
 

next/lf-current/Basics.v

@@ -2049,4 +2049,4 @@ Example test_bin_incr7 : bin_to_nat (B0 (B0 (B0 (B1 Z)))) = 8.
     output.  But since they have to be graded by a human, the test
     script won't be able to tell you much about them.  *)
 
-(* 2026-02-27 12:25 *)
+(* 2026-06-19 17:02 *)