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

Question

我的代码：

\n\n

law : \xe2\x88\x80 a x \xe2\x86\x92 ((suc a) * (suc a) \xc3\xb7 (suc a) \xe2\x9f\xa8 x \xe2\x9f\xa9) \xe2\x86\x92\xe2\x84\x95 \xe2\x89\xa1 (suc a , refl)\nlaw a x = refl\n

\n\n

我认为有太多suc a，我想给一个别名suc a，类似（这段代码只是描述了我的想法，它不能编译）：

\n\n

law : \xe2\x88\x80 a x \xe2\x86\x92 ((s : suc a) * s \xc3\xb7 s \xe2\x9f\xa8 x \xe2\x9f\xa9) \xe2\x86\x92\xe2\x84\x95 \xe2\x89\xa1 (s , refl)\nlaw a x = refl\n

\n\n

我能做到吗？

\n

Answer 1

当然。您可以使用let

\n\n

law : \xe2\x88\x80 a x \xe2\x86\x92 let s = suc a in (s * s \xc3\xb7 s \xe2\x9f\xa8 x \xe2\x9f\xa9) \xe2\x86\x92\xe2\x84\x95 \xe2\x89\xa1 (s , refl)\nlaw a x = refl\n

\n\n

或者定义一个匿名模块：

\n\n

module _ (a : \xe2\x84\x95) where\n  s = suc a\n  law : \xe2\x88\x80 x \xe2\x86\x92 (s * s \xc3\xb7 s \xe2\x9f\xa8 x \xe2\x9f\xa9) \xe2\x86\x92\xe2\x84\x95 \xe2\x89\xa1 (s , refl)\n  law x = refl\n

\n\n

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

\n