零域

content{:toc} 起因不知道大家是怎样安排自己的日常计划的，我习惯是建立一个仓库，按照年/周记录在 markdown 里，平时这个仓库也写点简单的 demo，目录类似如下： 123456 ...

These series of notes combined My notes on reading Software Foundation and (if any) watching on C ...

Review (only in slide)12Theorem review2: ∀b, (orb true b) = true.Theorem review3: ∀b, (orb b true) = ...

Pair of NumbersQ: Why name inductive?A: Inductive means building things bottom-up, it doesn’t have t ...

The critical new ideas arepolymorphism (abstracting functions over the types of the data they manip ...

apply exactly the same as some hypothesis can be used to finish a proof (shorter than rewrite then r ...

We have seen… propositions: factual claims equality propositions (e1 = e2) implications (P → Q) qua ...

Inductively Defined Propositions The 3rd way to state Evenness…Besides: 123Theorem even_bool_prop : ...