FStarLang / FStar

A Proof-oriented Programming Language
https://www.fstar-lang.org
Apache License 2.0
2.65k stars 232 forks source link

Allow empty record patterns #3321

Closed mtzguido closed 2 weeks ago

mtzguido commented 2 weeks ago

Related to #3320, I noticed we cannot write matches over a record without specifying one of its fields. The pattern {} does not even parse, and will not desugar even if it did. I think this comes from when we really needed to resolve the fields immediately to find the record type, but now that we have unresolved record constructors and projectors, we definitely can allow empty patterns.

The patch seems easy enough and we can now write something like this:

type t =
  | A { x:int; y:int }
  | B { z:bool }

let is_A (x:t) : bool =
  match x with
  | A {} -> true
  | _ -> false
mtzguido commented 2 weeks ago

I don't think this should be controversial, so merging.