カリーのパラドックス - Wikipedia Idrisでもやってみた。Agda版とほとんど一緒。 Agdaでsubstは、Idrisではreplaceになる。 a=bと(func) aを渡すと(func) bを返してくれる。 lemmaも定理もlet f = replace p x in f xで終わる所が美しい。 module Curry %de…