Jason Gross

[Feature Request] More kinds of regression / best-fit curve than just linear regression

6

**Brief outline of the proposed feature** It seems nice to be able to fit data to something other than just a line. (Note that the log mode for linear regression...

It would be nice for (1 -> C ᵒᵖ) to be the same as (1 -> C) ᵒᵖ

16

> We've actually gone out of our way in agda-categories to make as many of these things hold judgementally. For `1 -> C` vs `C`, that is hopeless, as they...

It would be nice to prove that Kan Extensions involving the terminal category align with (co)limits

1

> We've actually gone out of our way in agda-categories to make as many of these things hold judgementally. For `1 -> C` vs `C`, that is hopeless, as they...

Page 372 of HoTT ebook is cut off slightly

1

On [page 372 of the HoTT ebook](http://hottheory.files.wordpress.com/2013/03/hott-ebook-611-ga1a258c.pdf#page=386), `The quotient is generated by the following equalities (see Remark 8.7.3)` is slightly cut off.

simp only is quadratic in the size of the output term

2

### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover-community/lean/issues). *...

[request] c_call like c_func / fmt_c_decl

2

In usage in fiat-crypto, I find myself needing to recreate some of the logic from https://github.com/mit-plv/bedrock2/blob/13365e8113131601a60dd6b6ffddc5a0b92aed58/bedrock2/src/bedrock2/ToCString.v#L149-L156 I would like a function like ```coq c_arrange_arguments {A R} (args : list A)...

Does bedrock2 want warning/error annotations on PRs?

4

 (This is from fiat-crypto.) c.f. https://github.com/mit-plv/fiat-crypto/pull/703

Bytedump.v fails to build on Windows

2

Apparently, `^Z` (`\x1a`) is treated as end-of-file by coqc on Windows. This seems probably at least somewhat valid, given that [Wikipedia says](https://en.wikipedia.org/wiki/Substitute_character#End_of_file): > In CP/M, 86-DOS, MS-DOS, PC DOS, DR-DOS,...

bedrock2 fails to build when switching from EXTERNAL_DEPENDENCIES=1 to EXTERNAL_DEPENDENCIES= because _CoqProject is not remade

2

The rule for making `_CoqProject` considers it to be up-to-date whenever it exists. Therefore it is never remade, even when you, e.g., change the `Makefile` or switch to or from...

make is very noisy, even when there's nothing to be done

4

See also https://github.com/mit-plv/coqutil/issues/15; it's the same problem in the submakefiles here