2017-02-28 2 views
0

Quel est le sens de cet argument dans (a, b, c: Nat):Argument de type

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

?

Evidemment, le premier argument est un triplet, c'est-à-dire 3-tuple.

Répondre

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

est juste un raccourci pour

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

Si vous développez sur g: (a,b,c: Nat) -> Int vous obtiendrez

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

Un paramètre tuple nommé (AFAIK idris ne pas intégré triplets) serait spécifié comme

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