2007-09-17 [長年日記]
λ. Agda Implementors' Meeting 6
Codata や Observational Equality など、Agdaの型理論に欠けていると私が思っていたものについても、きちんと議論はされているのね。ちょっと安心した。
あと、Agataが GHC 6.6 で動かないのは、GHC 6.6 の Forall-Hoisting にバグがあるかららしい。へぇ。
Codata や Observational Equality など、Agdaの型理論に欠けていると私が思っていたものについても、きちんと議論はされているのね。ちょっと安心した。
あと、Agataが GHC 6.6 で動かないのは、GHC 6.6 の Forall-Hoisting にバグがあるかららしい。へぇ。