{"height":"190","blog_url":"https://kikx.hatenadiary.org/","provider_name":"Hatena Blog","type":"rich","author_url":"https://blog.hatena.ne.jp/kikx/","author_name":"kikx","provider_url":"https://hatena.blog","published":"2011-06-21 10:55:23","version":"1.0","title":" \u30bb\u30af\u30b7\u30e7\u30f3","image_url":null,"blog_title":"\u83ca\u3084\u3093\u306e\u96d1\u8a18\u5e33","html":"<iframe src=\"https://hatenablog-parts.com/embed?url=https%3A%2F%2Fkikx.hatenadiary.org%2Fentry%2F20110621%2F1308621323\" title=\" \u30bb\u30af\u30b7\u30e7\u30f3 - \u83ca\u3084\u3093\u306e\u96d1\u8a18\u5e33\" class=\"embed-card embed-blogcard\" scrolling=\"no\" frameborder=\"0\" style=\"display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;\"></iframe>","description":"Coq\u306e\u30bb\u30af\u30b7\u30e7\u30f3\u3068\u3044\u3046\u6a5f\u80fd\u3092\u4f7f\u3046\u3068\u30b0\u30ed\u30fc\u30d0\u30eb\u5909\u6570\u307f\u305f\u3044\u306a\u306e\u3092\u4f7f\u3048\u307e\u3059\u3002 Section Hoge. Variable x : nat. Definition foo := x + 1. Definition bar := foo + 2. (* Section \u306e\u4e2d\u3067\u306f x \u306f\u30b0\u30ed\u30fc\u30d0\u30eb\u5909\u6570\u307f\u305f\u3044\u306b\u4f7f\u3048\u308b *) End Hoge. (* Section \u3092\u9589\u3058\u308b\u3068\u3001foo \u3068 bar \u306f x \u3092\u5f15\u6570\u306b\u3068\u308b\u3088\u3046\u306b\u306a\u308b *) Definition baz := bar 42.\u3053\u306e\u6a5f\u80fd\u3068\u30dd\u30a4\u30f3\u30bf\u3092\u4e00\u7dd2\u306b\u4f7f\u3046\u3068\u5909\u66f4\u3067\u304d\u308b\u30b0\u30ed\u30fc\u30d0\u30eb\u5909\u6570\u307f\u305f\u3044\u306b\u4f7f\u3048\u307e\u3059\u3002 Section Foo. (* \u6700\u5f8c\u306b\u30b9\u30ed\u30c3\u30c8\u2026","categories":[],"width":"100%","url":"https://kikx.hatenadiary.org/entry/20110621/1308621323"}