Commit 2020-10-26 18:39 95b3add2

fix(tactic/derive_fintype): add support for props (#4777) This adds support for propositional arguments in inductive constructors. It was previously not handled, and while it almost works without change, we have to use Sigma' (a:A) (b:B) (c:C), unit to tuple up the arguments instead of Sigma' (a:A) (b:B), C because it would cause problems in the unary case where there is only one propositional field.