Kevin Meredith
Kevin Meredith

Reputation: 41909

Understanding Argument Type

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

Answers (1)

Markus
Markus

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

Related Questions