如何解决对默认参数使用默认注释是不好的形式吗?
在 the docs 中,它们展示了如何使用 default
注释来创建默认参数,例如
fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
fibonacci {lag} Z = lag
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
使得 fibonacci 5
与 fibonacci {lag=0} {lead=1} 5
相同。然后他们说
请注意,虽然这有效,但这不是 default
注释的预期用途。此处包含它仅用于说明目的。通常,default
用于提供自定义证明搜索脚本之类的内容。
像 default
示例中那样使用 fibonacci
创建默认参数是有问题的还是错误的形式?如果是,为什么?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。