Agda を勉強中です。いわゆる初心者マークです。どこぞのチュートリアルに載ってたこのコードが通らないので困る。最後の odd k の型が合わないらしい。 あと dotted pattern っていうのもいまいち理解に自信がない。型から値がわかるような仮引数につけるっ…

summer school library っていうのを使ったら動きました。あとでライブラリのコードを読まねば。 module Views where open import Data.Nat data Parity : ℕ -> Set where even : (k : ℕ) -> Parity (k * 2) odd : (k : ℕ) -> Parity (1 +…