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)

方法一用于指定nota的类型，方法二用于指定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 仅适用于绑定范围（在顶层，紧接在模块声明下，或紧接在函数右侧）。

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

What are the general forms for type ascription in Agda?

agda

agda-mode