Tesla Zhang‮

还忘了个事，Kotlin没有这种三段式的for循环，一般写 ```kotlin val Array.长度 = this.length; for (序号 in 0..二队.长度) 二队[序号]?.自我介绍(); ```

这个 `in` 就真的没办法了，这是一个语法

还没看，等会看

我没有write access。请在README里面添加代码块高亮谢谢。

``` Checking Web.Semantic.Everything (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/Everything.agda). Checking Web.Semantic.DL.ABox (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox.agda). Checking Web.Semantic.DL.ABox.Interp.Meet (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Meet.agda). Checking Web.Semantic.DL.ABox.Interp.Morphism (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda). Checking Web.Semantic.DL.TBox.Interp.Morphism (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/TBox/Interp/Morphism.agda). Checking Web.Semantic.DL.ABox.Model (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda). /home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda:143,1-14 Don't know how to parse inb (f , I⊨A). Could...

Is Agda completely losing the ability to use type inference to resolve overloaded operators? @UlfNorell Is this a language change?

``` ((pipe (J , j)) (K , k)) (J≲K , j≲k) ((pipe (J , j)) (K , k)) (J≲K , j≲k) ((pipe (J , j)) (K , k)) (J≲K ,...

My Agda compiler is built from 2d980891f570cf4a50b8e8843eb9c5269b4d888e commit in the compiler repo

Nice, thanks! In what case would hcom on HIT compute like an id function? My current understanding is that hcom on HIT is mostly canonical and sometimes reducible as id,...

A friend told me it's when your type is not parameterized, but I actually don't quite understand why it works this way. I guess I'll need to read some papers.