瞭解參數類型

Question

有哪些內容(a, b, c: Nat)參數的含義是：

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

？顯然，第一個參數是三元組，即3元組。

Answer 1

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

僅僅是

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

一條捷徑如果你在g: (a,b,c: Nat) -> Int擴大你會得到

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

命名元組參數（據我所知伊德里斯不具有內置的三倍）將被指定爲

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