相关疑难解决方法(0)

我正在尝试并且未能完成该traverse功能Data.Traversable.我无法理解其观点.由于我来自一个势在必行的背景,有人可以根据命令性循环向我解释一下吗？伪代码将非常感激.谢谢.

我试图解析Agda中的嵌套列表.我在谷歌搜索,我发现最接近的是在Haskell中解析,但通常使用像"parsec"这样的库,这些库在Agda中不可用.

所以我想"((1,2,3),(4,5,6))"用结果类型解析(List (List Nat)).

并且应该支持进一步的嵌套列表(直到深度5),例如,深度3将是(List (List (List Nat))).

我的代码非常冗长和繁琐,它只适用于(List (List Nat))但不适用于其他嵌套列表.我自己没有取得任何进展.

如果有帮助,我想splitBy从我的一篇旧帖子的第一个答案中重复使用.

NesList : ? ? Set
NesList 0 = ? -- this case is easy
NesList 1 = List ? -- this case is easy
NesList 2 = List (List ?) 
NesList 3 = List (List (List ?))
NesList 4 = List (List (List (List ?)))
NesList 5 = List (List (List (List (List ?)))) -- I …

我需要写一些东西用 agda 将数字转换为字符串。之前发现有人问过string转agda的方法。

Agda：解析带有数字的字符串

我想过反过来使用它，

row-to-stringh : (m : ?) ? string
row-to-stringh 0 = "0"
row-to-stringh 1 = "1"
row-to-stringh 2 = "2"
row-to-stringh 3 = "3"
row-to-stringh 4 = "4"
row-to-stringh 5 = "5"
row-to-stringh 6 = "6"
row-to-stringh 7 = "7"
row-to-stringh 8 = "8"
row-to-stringh 9 = "9"
row-to-stringh _ = ""

但它不够好。当数字大于 9 时，它只会将其转换为“”，而不是“（那个数字）”。有人可以帮我弄这个吗？