代码之家 › 专栏 › 技术社区 › M Farkas-Dyck

如何消除冲突构造函数名称的歧义

agda

M Farkas-Dyck · 技术社区 · 8 年前

参见示例 Data.Maybe.Base 在stdlib all中 Maybe Any 和 All 有一个 just 构造函数。

Agda允许这些定义。如何指定要使用哪一个?

1 回复 | 直到 8 年前

effectfully 8 年前

每种数据类型都有自己的模块。所以 Maybe , All Any Maybe.just , All.just 或 Any.just Thilo 在他们的评论中说。(然而,如果存在一些歧义,你会得到一个错误,这不是真的——你会得到一个未解决的元)。

推荐文章

Kyle McKean · 带表达式非求值

8 年前

ice1000 · 当Agda/Idris无法做到时,Coq可以做什么?

8 年前

Cactus · 构建数据。列表全部来自另一个数据。列表全部的

8 年前

ice1000 · Agda的“重写”失败,出现一个提到变量“w”的错误

8 年前

luochen1990 · 如何在Idris/Agda/Coq中模式匹配多个值?

8 年前

M Farkas-Dyck · 如何消除冲突构造函数名称的歧义

8 年前

Adi Ostrov · Agda:无法执行IO-数据丢失。海外金融机构,IO。外国金融机构

8 年前

user2667523 · Agda标准库-为什么更多属性没有标记为抽象?

10 年前

Aadit M Shah · 如何使用Agda中N的归纳原理证明N的递归器的定义方程命题成立?

10 年前

m0davis · 从论点的顺序解释这种奇怪的影响(如果可能的话,提供一个解决方法)

10 年前