product / tuple / pair type?

Stream: general

[JJ]

Hello! I would like to write something like | tuple (fields : List (Product (Option Key) Value)), but have been unable to find what the equivalent of a Tuple is in Lean...

[JJ]

I know I could do this by defining a structure Field where (key: Option Key) (value: Value) and pointing the List to that, but it feels unnecessary - I think I'm definitely missing some sort of inline product type. But, I've been searching through documentation and code and have been unable to find one. Any pointers would be appreciated!

[JJ]

(also - would this be the correct topic for questions & discussion of lean as a general purpose programming language?)

[Kim Morrison]

Prod

[Kim Morrison]

We just use iterated pairs for tuples (with a bit of syntax help).

[JJ]

Syntax help? :eyes:

[Kim Morrison]

i.e. you can just write (a, b, c) and Lean understands it as (a, (b, c))

[JJ]

Ah nice! is there any sugar for type declarations or would that just be (Prod A (Prod B C))?

[Kim Morrison]

A × B × C

[Kim Morrison]

I suggest reading #FPIL

[Kim Morrison]

Oops: https://lean-lang.org/functional_programming_in_lean/getting-to-know/polymorphism.html?highlight=Prod#prod

[Kim Morrison]

#fpil

[JJ]

Oh, I don't know how I missed that... looks like I missed everything after Options, whoops

[JJ]

Ty :sweat_smile:

[JJ]

Follow-up question: is it possible to define names ((a : A) × (b : B) × (c : C)) in product types or does that require a named structure?

[Kim Morrison]

No