instantiate a pair

Stream: new members

[Iocta]

How do I call this function?

universe u
variables α β : Type u
def f (x: α × β ) : true := trivial

[Iocta]

aha, langle/rangle

[Iocta]

universe u
variables α β : Type u
def f (x: int × int ) : true := trivial

#check f ⟨1 ,2 ⟩

[Anne Baanen]

\langle / \< and \rangle / \> work for all inductive types with one constructor, but × has special syntax support in Lean so you can write tuples "naturally":

#check f (1, 2)