如何在 Agda 类型声明中定义别名？

Question

我的代码：

law : ∀ a x → ((suc a) * (suc a) ÷ (suc a) ⟨ x ⟩) →ℕ ≡ (suc a , refl)
law a x = refl

我觉得suc a太多了，我想给suc a起个别名，比如（这段代码只是描述我的想法，它不会编译）：

law : ∀ a x → ((s : suc a) * s ÷ s ⟨ x ⟩) →ℕ ≡ (s , refl)
law a x = refl

我能做到吗？

Answer 1

当然可以。您可以使用 let

law : ∀ a x → let s = suc a in (s * s ÷ s ⟨ x ⟩) →ℕ ≡ (s , refl)
law a x = refl

或者定义一个匿名模块：

module _ (a : ℕ) where
  s = suc a
  law : ∀ x → (s * s ÷ s ⟨ x ⟩) →ℕ ≡ (s , refl)
  law x = refl

模块外部 law 与您提供的类型签名相同。