Isabelleを書く

code:memo.thy

theory T

imports T 1 . . . T n

begin

definitions, theorems and proofs

end

少しHaskellっぽい記法になっている

code:memo.thy

fun add :: "nat ⇨ nat ⇨ nat" where

"add 0 n = 0"

| "add (Suc m) n = Suc (add m n)

どうしてこういう定義になるかわからない。