说明:原型
它是一种简单的依赖类型语言的类型检查器。 类型检查过程与[1]的过程非常相似:它是双向的且基于NbE,因此我们具有原始术语和值,但是由于我们处于依赖类型设置中,因此也存在由表示内容的值索引的类型化术语类型。 例如,类型Π型是
data _⊢_ {n} (Γ : Con n) : Value n -> Set where
πᵗ : (σₜ : Γ ⊢ typeᵛ) -> Γ ▻ eval σₜ ⊢ typeᵛ -> Γ ⊢ typeᵛ
...
该示例说明,评估是在类
<weixin_42099070> 上传 | 大小:10kb