Guest0x0

(* 这是我（预期，亦或是已经）在 ∞-type càfe summer school 上做的 talk，

     "从零教你手把手实现一个 MLTT 类型检查器"

   的内容稿。本 talk 计划以现场边讲解边手写代码的方式实现，
   所以虽然这份内容稿会尽量尝试还原 talk 的思路和逻辑，
   它的内容可能会与实际的 talk 有出入，建议有条件的人直接去听 talk 本身 *)

(* 本次 talk 将会使用 OCaml 来实现一个 MLTT 类型检查器。
   你可能不会写 OCaml，但这没有关系。本次 talk 只会使用以下的功能：