Joseph Myers
Joseph Myers
It might make sense to put this form of Ceva in `archive/` until we have more general versions in mathlib, but various lemmas that suggest more general results should be...
Note that the specific lemmas I commented on are cases where something seems appropriate for mathlib proper even if it doesn't end up getting used in proving more general versions...
The following is for any affine space over a field, with no requirements for any order on the field (and thus not involving distance or interior), and some lemmas may...
If you want to avoid leading newlines at the start of the overall output, that could be done in `convert_soup`.
I'd like to reiterate what I said at https://sourceware.org/ml/libc-alpha/2017-09/msg01029.html regarding the context for the above quoted comments. They are about a hypothetical situation: suppose we had consensus for inclusion of...
[test29.txt](https://github.com/libdfp/libdfp/files/67514/test29.txt) Test attached as .txt since GitHub doesn't allow attaching .c files.
This fix looks wrong for FE_TONEAREST mode, when conversion of a value with absolute value less than or equal to half the least subnormal in the target type should produce...
PR #120 should help here, it fixes various cases of block tags not being properly separated from adjacent content, including headers.
I think this issue, #155 and #95 should all be dealt with together. #95 involves ``, which gets converted to significant whitespace, so illustrating that at this stage it is...
Should be fixed by my PR #120.