Commit 2024-08-16 01:08 925a304c

feat: Finset builder notation (#11582) Define elaborators (but no delaborators) to elaborate the following notations to a Finset: In Data.Finset.Basic,

• {x ∈ s | p x} In Data.Fintype.Basic,
• {x | p x}
• {x : α | p x}
• {x ∉ s | p x}
• {x ≠ a | p x} In Order.Interval.Finset.Basic,
• {x ≤ a | p x}
• {x ≥ a | p x}
• {x < a | p x}
• {x > a | p x} The general heuristic for deciding whether to elaborate a given notation as a Set or Finset is:
• Check whether the expected type is Finset ?α.
  • If it is, elaborate as a Finset.
  • If it isn't, check whether the expected type of s in the notation is Finset ?α.
    • If it is, elaborate as a Finset.
    • If it isn't or there is no s in the notation, elaborate as a Set. There is currently a gotcha that elaboration to Set is highly preferred because we can't postpone metavariable and override the set elaborator without breaking many existing uses of set builder notation. See Zulip.