Commit 2022-03-14 13:59 df3792f8

refactor(data/set): generalize set.restrict and take set argument first in both set.restrict and subtype.restrict (#12510) Generalizes set.restrict to Pi types and makes both this function and subtype.restrict take the restricting index set before the Pi type to restrict, which makes taking the image/preimage of a set of Pi types easier (s.restrict '' pis is shorter than (λ p, set.restrict p s) '' pis -- I'd argue that this is the more common case than taking the image of a set of restricting sets on a single Pi type). Changed uses of set.restrict to use dot notation where possible.