Commit 2023-05-26 01:31 ca570a16

feat: fbinop% term elaborator to support set product notation (#4308) This introduces a term elaborator like the binop% term elaborator to help elaborate expressions involving "functorial" types, like Set, Finset, List, etc., and coercions between them. The binop% elaborator tries to solve for the minimal type where an arithmetic expression makes sense given which coercions exist. The fbinop% elaborator tries to solve for the minimal "functor." This is designed specifically to support the generic s ×ˢ t set product notation. Using just a class is unsufficient because often you want the expected type to help drive the coercions. This also is able to supply hints to the arguments to help homogenize the operator. Some examples:

example (s : Finset α) (t : Set β) (u : Finset γ) : Nat.card (s ×ˢ t ×ˢ u) = 0
-- After elaboration: Nat.card ↑(↑s ×ˢ t ×ˢ ↑u) with the Finsets as Sets
example (s : Set α) (t : Set (α × ℕ)) : s ×ˢ {1, 2, 3} = t
-- The {1, 2, 3} is a Set
example (s : Finset α) (t : Finset (α × ℕ)) : s ×ˢ {1, 2, 3} = t
-- The {1, 2, 3} is a Finset

These would fail without the fbinop% elaborator. To support subobjects in the algebraic hierarchy, a "functorial type" may have any number of instance arguments after the type argument.