2009-10-13から1日間の記事一覧
data Nat : Set0 where zero : Nat succ : Nat -> Nat data NatHold : Nat -> Set0 where natHold : (n : Nat) -> NatHold n test : (x : Nat) -> NatHold x test x with x test x | zero with x test x | zero | zero = natHold zero test x | zero | succ …