目前为止本质都是和 agda 同构的。感受是 coq 用起来方便的多，不会去打一些奇怪的字符，此外我个人认为 coq 的语法设计更优雅、人性化一点。看看后面会讲什么吧。