最近這裡好像比較熱鬧，希望有大大能看到我的問題 orz
廢話有點多，如果想直接看問題的話請直接拉到最下面
假設有一個 Id : String → Set，用來表示 Minecraft 中的各種不同物品
data Id : String → Set where
　id : (rawId : String) → Id rawId
對於一種物品我們須要知道的事只有三個，名字、物品欄中的可堆疊數量、是否能在創造
模式物品欄中直接獲得
record Item {rawId : String} (_ : Id rawId) : Set where
　field
　　displayName : Id rawId → String
　　stacks : Id rawId → Fin 65
　　obtainable : Bool
開始新增物品種類到 Minecraft 世界中
instance
用 "minecraft:stone" 建立的 Id 當作石頭的 ID，石頭可以堆疊 64 個，可從創造模式
物品欄直接活獲得
　Stone : Item (id "minecraft:stone")
　Stone =
　　record {
　　　displayName = "Stone";
　　　stacks = # 64;
　　　obtainable = true
　　}
盔甲座 ID 是 "minecraft:armor_stand"，可堆疊 16 個，可以從創造模式物品欄直接獲
得
　ArmorStand : Item (Id "minecraft:armor_stand")
　ArmorStand =
　　record {
　　　displayName = "Armor Stand";
　　　stacks = # 16;
　　　obtainable = true
　　}

來發正念召喚看看 banacorn 或 petercommand ...petercommand 說 https://bit.ly/2xc9qDcptrcmd> 就..直接把 instance 傳進去阿..XD

感謝回答！ 抱歉沒講清楚，rawId 有可能是 runtime 的輸入如果把 itemDisplayName 的 type 改成 String -> Maybe String 的話有解嗎 @@主要就是希望保留 instance resolution，而且須要某種方法在 runtime 知道 resolution 成功與否（雖然說 resolution 是在 compile time orz...）是不是須要 reflection 啊

來發正念召喚看看 banacorn 或 petercommand ...petercommand 說 https://bit.ly/2xc9qDcptrcmd> 就..直接把 instance 傳進去阿..XD

感謝回答！ 抱歉沒講清楚，rawId 有可能是 runtime 的輸入如果把 itemDisplayName 的 type 改成 String -> Maybe String 的話有解嗎 @@主要就是希望保留 instance resolution，而且須要某種方法在 runtime 知道 resolution 成功與否（雖然說 resolution 是在 compile time orz...）是不是須要 reflection 啊

不知道為什麼想到 type provider. 沒有很懂問題描述XD

Agda 的 reflection 只有在 type-checking 階段發生

不知道為什麼想到 type provider. 沒有很懂問題描述XD

Agda 的 reflection 只有在 type-checking 階段發生

不知道為什麼想到 type provider. 沒有很懂問題描述XD

Agda 的 reflection 只有在 type-checking 階段發生