Reputation: 41909
What's the meaning of this (a, b, c: Nat)
argument in:
g : (a, b, c: Nat) -> Int
g (a,b,c) = 42
?
Evidently the first argument is a triple, i.e. 3-tuple.
Upvotes: 0
Views: 59
Reputation: 1303
g: (a,b,c: Nat) -> Int
is just a short cut for
g: (a: Nat) -> (b: Nat) -> (c: Nat) -> Int
If you expand on g: (a,b,c: Nat) -> Int
you will get
g: (a, b, c: Nat) -> Int
g a b c = ?g_rhs
A named tuple parameter (AFAIK idris does not have built-in triples) would be specified as
g: (a: (Nat, Nat)) -> Int
g a = ?g_rhs
Upvotes: 3