Agda apkg はだめ

結局、DivMod 通らないので apkg はあきらめ。とりあえず、Homebrew から入れなおし。

Solver とか面白いんだけど、

　open AlmostCommutativeRing ring
　-- The solver is flexible enough to work with ℕ (even though it asks
　-- for rings!)
　lemma₁ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x
　lemma₁ = solve-∀

こいつって、Data.Nat じゃないんだな。これを Data.Nat に引き戻す方法がわからない。

もっとも、もっと、ずっと簡単にできる方法がある気もする。

いや、~/.cabal が悪さをしていたらしい。削除で解決。