Mario Carneiro
Mario Carneiro
> fix: use semireducible transparency when producing no_confusion_type and injectivity lemmas #812 You mean *reducible* transparency, right?
*Note: this may be suitable either as a comment on #2691 or here. I'm assuming interested parties are watching both anyway.* The restriction on caller and callee having the exact...
> @digama0 > > > * You can't get a function pointer with "rusttail" convention > > * You can't use a "rusttail" function cross-crate > > This feels unnecessary...
Nothing about this feature is unsafe or even meaningfully interacts with unsafe parts of the language. What footguns are you referring to? The worst that can happen if you mess...
I think having it be optional is defensible: * It should be allowed to be omitted because there is a legitimate aesthetic/readability argument against it (`inductive Foo where` looks like...
`where` after `def` is valid, and is used for defining structure instances: ```lean def foo : Inhabited Nat where default := 0 ```
Beware of mathportisms when looking at mathlib code for common style. I just checked and no-`where` is mathport style, so this will disproportionately affect the measurement. (I don't recall giving...
Note, in lean 3 there was only no-`where` syntax, so I think your theory doesn't match. I'm pretty sure that when `where` was introduced core used it across the board,...
The idea is that `int.floor` and `int.fract` should compute on rational numerals, for example `int.floor (5 / 2) = 2` and `int.fract (5 / 2) = 1 / 2`.
hey, I wrote that :smile: