M F*_*yck 1 agda
例如见Data.Maybe.Base在STDLIB -所有的Maybe,Any和All有一个just构造函数.
Maybe
Any
All
just
Agda允许这些定义.如何指定使用哪一个？
use*_*465 5
每种数据类型都有自己的模块.所以Maybe,All并且Any都是类型构造函数和模块同时存在.因此,你可以写Maybe.just,All.just或Any.just消除歧义的构造.或者它可以通过类型推断(统一是一个更合适的术语)或像Thilo在评论中所说的显式类型签名来消除歧义.(然而,如果出现歧义,你会得到一个错误 - 你会得到一个未解决的元).
Maybe.just
All.just
Any.just
归档时间：
8 年，4 月 前
查看次数：
61 次
最近记录：