最近这里好像比较热闹，希望有大大能看到我的问题 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 阶段发生