無法使用IdrisNet2創建簡單的二進制數據結構

Question

我正嘗試使用IdrisNet2庫來定義一些二進制數據結構。我正在使用IdrisNet2的Idris 0.9.17.1和commit 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

對不起。前一陣子，我們決定對所有類型及其構造函數進行大寫標準化;這意味着oh和so被重命名爲Oh和So。所以有一個更新到這個庫讓它來編譯，但它看起來像一個oh在默認策略來解決一個隱含的參數被忽視： https://github.com/SimonJF/IdrisNet2/blob/master/src/IdrisNet/PacketLang.idr#L149 因此，戰術總是會失敗（oh是一個未定義的參考）。您可以明確地將p的值傳遞給那裏，那將起作用：bits 16 {p = Oh}。

但我已經提交了一個pull請求來解決lib中的問題：https://github.com/SimonJF/IdrisNet2/pull/11