mathlib3
d4568a41
- fix(data/subtype): don't use pattern matching in subtype.map (#725)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
fix(data/subtype): don't use pattern matching in subtype.map (#725)
References
#725 - fix(data/subtype): don't use pattern matching in subtype.map
Author
rwbarton
Committer
johoelzl
Parents
5da8605f
Loading