有了以下相等的定义,我们就有了refl作为构造函数。 refl : x ≡ xcong : ∀ { a b} { A : Set a } { B : Set b }cong f refl = refl
我不确定我能不能准确地分析这里到底发生了什么。我认为我们是在隐藏参数上进行模式匹配:如果我们用另一个标识符替换第一次出现的情况,就会得到一个类
人们如何在Agda中形成一个依赖类型的逻辑,而不是通过重用Agda类型系统本身来“作弊”呢?a ∷ a ∷ γ ⊢ b → a ∷ γ ⊢ b我还可以大致遵循教程在Haskell中实现可靠类型的但是它是隐式的,不像我的Agda代码,我甚至不知道从哪里开始修改我的代码,因为到目前为止我想到的路径导致了无限的倒退:
data _⊢_ : List (? ⊢ ?) → (? ⊢ ?