functional-programming - 如何在 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具有与您提供的相同的类型签名。