好吧，不行……这 PrismJS 貌似也是个菜鸡

让我们来试试高亮 Agda {-# OPTIONS --without-K --rewriting #-}

pen import lib.Basics pen import lib.types.Int pen import lib.types.Pi

odule lib.types.Group where

• 1-approximation of groups without higher coherence conditions. ecord GroupStructure {i} (El : Type i) --(El-level : has-level 0 El) : Type i where constructor group-structure field ident : El inv : El → El comp : El → El → El unit-l : ∀ a → comp ident a == a assoc : ∀ a b c → comp (comp a b) c == comp a (comp b c) inv-l : ∀ a → (comp (inv a) a) == ident

  ⊙El : Ptd i ⊙El = ⊙[ El , ident ]

  private infix 80 _⊙_ _⊙_ = comp

  abstract inv-r : ∀ g → g ⊙ inv g == ident inv-r g = g ⊙ inv g =⟨ ! unit-l (g ⊙ inv g) ⟩ ident ⊙ (g ⊙ inv g) =⟨ ! inv-l (inv g) |in-ctx ⊙ (g ⊙ inv g) ⟩ (inv (inv g) ⊙ inv g) ⊙ (g ⊙ inv g) =⟨ assoc (inv (inv g)) (inv g) (g ⊙ inv g) ⟩ inv (inv g) ⊙ (inv g ⊙ (g ⊙ inv g)) =⟨ ! assoc (inv g) g (inv g) |in-ctx inv (inv g) ⊙ ⟩ inv (inv g) ⊙ ((inv g ⊙ g) ⊙ inv g) =⟨ inv-l g |in-ctx (λ h → inv (inv g) ⊙ (h ⊙ inv g)) ⟩ inv (inv g) ⊙ (ident ⊙ inv g) =⟨ unit-l (inv g) |in-ctx inv (inv g) ⊙_ ⟩ inv (inv g) ⊙ inv g =⟨ inv-l (inv g) ⟩ ident =∎

好吧，知乎的貌似也是个菜鸡……这篇专栏里的高亮也不对。

我也找不到更好的高亮插件了，我稍微写复杂点它就没法parse了。 Jekyll 能用的高亮插件我记得的有两个，当初研究 Agda 的时候折腾了下，结果全都不支持 Agda 。 Python 写的那个被抛弃了，我现在用的是 Rouge 。

fun main(args: Array<String>) { val list = object : ArrayList<String>(), Cloneable { override fun clone(): Any { return super<ArrayList>.clone() } } System.out.println(list) run breaking@ { (0..20).forEach continuing@ { if (10 <= it) return@breaking println(it) } infix fun Int.+(int: Int) = this * int n Array<String>.main() { println(1 + 10) // 输出 10 println(1 + 10) // 输出 11 这些高亮在 qlbf 的博文里全部有问题。

正确的引用样式是什么？

虎哥你这个quote的辣眼睛的两个引号什么时候可以弄掉啊。

这么写渲染居然没有出问题。 在格上，Kleene 不动点定理(Kleene's fixed point theorem)的内容是： 如果 (L, sqsubseteq) 是一个完备格，并且函数 f : L to L 是连续的，那么有：<br/>

athit{lfp}(f) = mathit{sup}(K(bot))

我可能找到了，在这里。Web 语言写的，该怎么让它发挥作用呢？

肯定啊。双缓冲是个很简单的东西嘛。。。