あまりわかってないけど、とりあえずいくつか適当な関数を書いたのでメモ。依存型うける(気がする)。 agda2 の emacs モードが使いこなせないのと関数を実行する方法がわからんのが問題である。 module NList where data Nat : Set where zero : Nat succ : …
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。