{"blog_url":"https://yosh.hateblo.jp/","author_url":"https://blog.hatena.ne.jp/yoshihiro503/","width":"100%","url":"https://yosh.hateblo.jp/entry/20090411/p1","provider_url":"https://hatena.blog","title":"SICP\u306eEx 2.4 \u3092Coq\u3067\u89e3\u3044\u3066\u307f\u305f","provider_name":"Hatena Blog","html":"<iframe src=\"https://hatenablog-parts.com/embed?url=https%3A%2F%2Fyosh.hateblo.jp%2Fentry%2F20090411%2Fp1\" title=\"SICP\u306eEx 2.4 \u3092Coq\u3067\u89e3\u3044\u3066\u307f\u305f - \u306b\u308f\u3068\u308a\u5c0f\u5c4b\u3067\u306e\u30d7\u30ed\u30b0\u30e9\u30df\u30f3\u30b0\" class=\"embed-card embed-blogcard\" scrolling=\"no\" frameborder=\"0\" style=\"display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;\"></iframe>","blog_title":"\u306b\u308f\u3068\u308a\u5c0f\u5c4b\u3067\u306e\u30d7\u30ed\u30b0\u30e9\u30df\u30f3\u30b0","type":"rich","author_name":"yoshihiro503","categories":["Coq","SICP","Extraction Language Scheme"],"height":"190","published":"2009-04-11 00:00:00","image_url":null,"description":"SICP\u3092\u8aad\u3093\u3067\u3044\u305f\u3089 \u691c\u8a3c\u305b\u3088 \u3068\u3044\u3046\u554f\u984c\u304c\u3042\u3063\u305f\u306e\u3067\u3001Coq\u3067\u691c\u8a3c\u3057\u3066\u307f\u305f\u3002\u554f\u984c\u306f\u30da\u30a2\u69cb\u9020\u306e\u30c1\u30e3\u30fc\u30c1\u30a8\u30f3\u30b3\u30fc\u30c7\u30a3\u30f3\u30b0\u306e\u8a71\u3002Scheme (untyped \u03bb) \u306b\u6bd4\u3079\u3066 Coq (\u03bbC) \u306f\u578b\u304c\u53b3\u683c\u306a\u306e\u3067\u3001\u554f\u984c\u306e\u5b9a\u5f0f\u5316\u304c\u3061\u3087\u3063\u3068\u5927\u5909\u3060\u3063\u305f\u3051\u3069\u3001\u554f\u984c\u81ea\u4f53\u306f\u7c21\u5358\u306b\u8a3c\u660e\u3067\u304d\u305f\u3002 Coq\u306e\u30b3\u30fc\u30c9\u304b\u3089Scheme\u306e\u30b3\u30fc\u30c9\u3092\u51fa\u529b\u3057\u3066\u307f\u305f\u3089\u3001\u554f\u984c\u3067\u4e0e\u3048\u3089\u308c\u3066\u3044\u308b\u30b3\u30fc\u30c9\u3068\u3060\u3044\u305f\u3044\u4e00\u7dd2\u3060\u3063\u305f\u304b\u3089\u5927\u4e08\u592b\u3060\u308d\u3046\u3002 Section SICP_EX_2_4. (* \u3053\u306e\u30bb\u30af\u30b7\u30e7\u30f3\u3067\u4f7f\u3046\u4e8c\u3064\u306e\u578b A, B \u3092\u4eee\u5b9a\u3059\u308b *) Variable A B : Type. Definition pair (X:Type) :\u2026","version":"1.0"}