我々は、様々なレベルのコンテキスト（ライブラリ、モジュール／セクション）を行為〈activity〉により拡張していくのだが、拡張のための行為は二種類しかない。 関数定義 （λΠ計算ベース） 帰納的型定義 （CICベース） 関数定義は def で、帰納的型定義は i…

名前付き引数〈named arguments〉と引数省略時値〈default value〉の指定 def mySub (left right :Nat) : Nat := left - right #check mySub #eval mySub (right := 3) (left := 5) --> 2 def mySub' (left :Nat) (right:Nat := 1) : Nat := left - right #c…