Hi, I was wondering what the difference is between math-comp analysis's 'classical sets' and math-comp's 'subTypes' as in mathcomp/ssreflect/eqtype.v. Why are there two approaches to working with subsets?
mathcomp/ssreflect/eqtype.v
Last updated: Oct 13 2024 at 01:02 UTC