Zulip Chat Archive

Stream: new members

Topic: instantiate a pair


view this post on Zulip Iocta (Aug 20 2020 at 08:41):

How do I call this function?

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

view this post on Zulip Iocta (Aug 20 2020 at 08:45):

aha, langle/rangle

view this post on Zulip Iocta (Aug 20 2020 at 08:46):

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

#check f 1 ,2 

view this post on Zulip Anne Baanen (Aug 20 2020 at 08:58):

\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)

Last updated: May 08 2021 at 04:14 UTC