2010-07-20から1日間の記事一覧
module IndHatena where open import Data.Nat import Level open import Induction.Nat using (<-rec) f : (x : ℕ) -> ℕ f zero = zero f x = f x' where postulate x' : ℕ postulate pr : x' < x f改' : (x : ℕ) -> ((y : ℕ…