第 3 回
関数の拡張，述語論理

• プリント

• 1 関数の拡張
  
  • (型，ソート) の例 … 長さ n のリストの型
  • (ソート，型) の例 … 4 節の例の f
        Section id_section.
            Variable A : Set.
            Definition f : A -> A := fun n : A => n.
        End id_section.
    6 節の le_n と le_S も依存型。
  • (ソート，ソート) の例 … 'a list の list
    例えば，bool というソートから bool list というソートが出来る。
• 4 節の f と 5 節の id_P は，一対一に対応付けられる。
  (多相関数は，forall の付いた命題の証明と一対一に対応がつく。)