内容： 型宣言とホーアトリプル 関数定義とホーアトリプル ホーア論理とホーアセオリー 伴意順序 いろいろな概念を統合できるかな 型宣言とホーアトリプルfが関数だとして、f:X→Y という形はfの型宣言だとみなせます。話を簡単にするために、「型とは集合だ…