Agda中类型归属的一般形式是什么？

Question

背景：我正在研究 Prabakhar Ragde 的 "Logic and Computation Intertwined"，这是对计算直觉逻辑的精彩介绍。在他的最后一章中，他介绍了使用 Agda 的一些基础知识。我已经成功安装了 Agda 并设法扭转了 emacs 的手臂（花了很多力气！）以使 agda-mode 工作得相当好，但我觉得我错过了各种类型归属表格的摘要阿格达。

具体来说，在不爆炸的情况下在 Agda 中完成一个证明需要相当多的类型归属——让我们暂时说它有这种类型，好吗？——我发现自己缺少将类型与名称相关联的能力以统一的方式。我现在知道有两种方法可以做到这一点，但我觉得好像缺少一种更通用的方法。

• 方法一：使用“where”形式时，可以使用双行规范进行类型归属。
• 方法 2：当使用显式 lambda 时，我可以使用括号和冒号将类型赋予标识符。

以下说明了这两种情况（使用简单但未包括在内的or 和否定的定义，抱歉）：

ex9 : ∀ (A B : Set) → ¬ (¬ (or A (¬ A)))
ex9 A B aornotaimpliesbottom = aornotaimpliesbottom (or-intro-2 nota)
  where nota : ¬ (A)
        nota = λ (a : A) → aornotaimpliesbottom (or-intro-1 a)

方法1用于指定nota的类型，方法2用于指定nota的参数类型。

但问题是：如果我想在“表达式”位置使用类型归属怎么办？例如，如果我想指定术语 (or-intro-1 a) 的类型怎么办？我可以使用“where”子句将其拉出到自己的绑定中，但是....哦，实际上，这似乎不起作用；将“where”嵌入到 lambda 中没有按预期工作。哦！看起来“让”在那里工作。好吧，无论如何，问题仍然存在：是否有一种更轻量级的方式来指定内联表达式的类型？

Answer 1

可以如下定义内联类型注解：

infixl 0 _∋_
_∋_ : ∀{i}(A : Set i) → A → A
A ∋ x = x

或者从标准库中导入：

open import Function using (_∋_)

然后A ∋ exp 可以作为任何表达式的内联类型注释。例如，在您的代码中为：

nota = λ (a : A) → aornotaimpliesbottom (or A (¬ A) ∋ or-intro-1 a)

您还可以插入内联类型注释，或有效地查询代码中已经存在的表达式的类型，方法是首先插入如下所示的孔：

nota = λ (a : A) → aornotaimpliesbottom (? ∋ or-intro-1 a)

然后在洞中点击C-c-s，使用默认推理填充洞。

还要记住let 在语法上比where 更灵活。您可以将let 放在任何表达式中，但where 仅适用于绑定范围（在顶层、模块声明下或函数右侧）。