RFC: Partial destructuring

Stream: lean4

[Denis Gorbachev]

structure Person where
  name : String
  age : Nat

def Centennial (person : Person) : Prop :=
  -- let { age } := person -- doesn't work, proposing to implement it
  let { name, age } := person
  age ≥ 100

We already have destructuring assignment, which is great: let { name, age } := person. However, partial destructuring assignment doesn't work: let { age } := person is a syntax error.

Partial destructuring would improve readability, especially for functions on structures with 3+ fields, especially where one field is used multiple times throughout the function.

What do you think?

[James Gallicchio]

you can do { age, .. } which is pretty close :)

[Denis Gorbachev]

@James Gallicchio Thanks for the pointer!

[Denis Gorbachev]

Wouldn't it be shorter if we could just write { age }?

[James Gallicchio]

It would be shorter, but it is nice to have exhaustivity checks for destructuring patterns by default. It helps you find all the places that might need updating when you change a structure!