idris - 无法使用 IdrisNet2 创建简单的二进制数据结构

Question

我正在尝试使用IdrisNet2库来定义一些二进制数据结构。我正在使用 Idris 0.9.17.1 并提交 IdrisNet2 的 262b746c9a2405e43d1de6a48de44cac2fd19932。我正在定义一个带有一个 16 位字段的数据包：

module Main
import IdrisNet.PacketLang
import Data.So

myPacket : PacketLang
myPacket = with PacketLang do
    bits 16

main : IO ()
main = putStrLn "hello"

我得到编译器错误：

 Can't solve goal 
       So (fromInteger 16 > fromInteger 0)

究竟是什么问题，我该如何解决？我猜我需要向编译器证明 16 大于 0，但我不确定如何在 Idris 中执行此操作或为什么这是必要的。

Answer 1

对于那个很抱歉。不久前，我们决定将所有类型及其构造函数的大写标准化；这意味着ohandso被重命名为Ohand So。因此，对此库进行了更新以使其编译，但它看起来像oh在默认策略中解决隐式参数被忽略： https ://github.com/SimonJF/IdrisNet2/blob/master/src/IdrisNet /PacketLang.idr#L149 所以这个策略总是会失败（oh是一个未定义的引用）。您可以显式传递p那里的值，这将起作用：bits 16 {p = Oh}.

但我已经提交了一个拉取请求来解决这个问题：https ://github.com/SimonJF/IdrisNet2/pull/11