Login
Create new posts
或者说现有的许多编程语言都不是很稳，因为静态分析和类型系统还是太初级了。
我们可能需要 refinement type，比如「至少有一个 (own) key 的 Object」，这个 TypeScript 似乎还无法表达。
graphql-js 的接口似乎要求至少有一个 fields，然而这样的错误无法在编译时检查出来，结果在运行时报了错。
当然这也可能是它接口设计的不足。
另一方面，如果我们实现了这种类型，似乎势必就要求有证明系统，不然你提供非字面量参数的时候，编译器怎么知道它至少有一个 (own) key 呢？甚至应该像 Dafny 那样提供根据条件、结论提示的自动证明系统。不过这样编译时间可能会变得无法忍耐啊……何况现在单核性能已经到瓶颈了。也许证明系统的并行化也是一个值得考虑的方向。
pm2 的 reload 功能好像不是很稳，重启有错也能重启。或者说这其实是运行时错误，pm2 不把它当成重启失败。
好吧，不行……这 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 语言写的，该怎么让它发挥作用呢？
Create new posts