理解引数の型

Question

はこの(a, b, c: Nat)引数の意味は何ですか？明らかに第1引数は3倍、すなわち3タプルである。

Answer 1

g: (a,b,c: Nat) -> Int 

（私の知る限りイドリスが組み込まれていませんトリプル）あなたはg: (a,b,c: Nat) -> Intに展開する場合は、

g: (a, b, c: Nat) -> Int 
g a b c = ?g_rhs 

という名前のタプルパラメータを取得します

g: (a: Nat) -> (b: Nat) -> (c: Nat) -> Int 

のためだけの近道です

g: (a: (Nat, Nat)) -> Int 
g a = ?g_rhs