Simon Hudon
On the other hand, could we say that `open_locale` always opens the namespace of the name of the locale? We could add an option to inhibit that behavior but we...
I don't think that would be too big a change. You'd have to provide an alternative definition of `tfae` (call id `tfae'`) which takes a list of pairs of names...
`field` indeed lacks documentation: https://github.com/leanprover-community/mathlib/blob/master/src/tactic/interactive.lean#L437
Why is this useful?
I feel like the performance improvement would be minimal and it might just make your proofs more brittle. You change your hypothesis names and it breaks. If you don't know...
@jcommelin I like your suggested syntax. My only worry is that, because the number of cases is `n!` for `n` variables, it's easy to make it unreasonably slow or otherwise...
I can't think of one. The only thing is that it might not be the right notion of extensionality for you
If we could change the meaning of `structure`, I'd be in favor with redefining it the way you say but I don't want to start redefining basic structures for something...
I should probably take care of * [ ] category/monad/basic.lean * [ ] category/bitraversable/lemmas.lean * [ ] category/bitraversable/instances.lean