mathlib3
dc57de22 - feat(logic/basic): When a dependent If-Then-Else is not one of its arguments (#10924)

Commit

4 years ago

feat(logic/basic): When a dependent If-Then-Else is not one of its arguments (#10924) This is the dependent version of #10800.

Author

YaelDillies

Parents