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.
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.
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