问Idris2中的泛型增量函数
EN

Stack Overflow用户

提问于 2021-07-05 05:27:02

回答 1查看 40关注 0票数 0

只要学习Idris 2并尝试实现一个可以处理任何实数/整数的通用增量函数，据我所知，Num类型应该涵盖小数，所以我认为这可以满足定义要求：

inc : Num ty => ty -> ty
inc x = x + 1

但是当用两个数字运行它时，它会失败。

Main> inc 2.3
Error: Can't find an implementation for FromDouble Integer.

(Interactive):1:5--1:8
 1 | inc 2.3

有没有办法扩展Num来做到这一点，或者是否存在另一种类型可以帮助我？

发布于 2021-07-05 05:43:59

这对我来说很有效：

inc : Num ty => ty -> ty
inc x = x + 1

x : Double
x = inc 2.3

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/68248903

复制

相似问题

问Idris2中的泛型增量函数EN