Jason Gross
Jason Gross
I find the `match!` feature of company-coq very useful when coding in Coq; it'd be nice to have a way to auto-populate a `match` statement with all of the branches...
Consider this Lean file: ```lean def some_lets : ℕ → ℕ → ℕ | 0 v := v | (nat.succ n) v := let k := some_lets n v +...
I'd like something like Coq's `Search` or `SearchAbout`: something that lists all of the theorems currently imported/accessible that match a particular pattern, and their types. (Apologies if something like this...
```lean universes u v inductive let_inM : Sort u → Sort (u+1) | ret : Π {A : Sort u} , A → let_inM A | bind : Π {A...
### Prerequisites * [ ] 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/lean4/issues)....
### Prerequisites * [ ] 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/lean4/issues)....
Since the CI update, we're getting duplicate warning annotations from the opam package jobs. I think this needs to be solved upstream at https://github.com/coq-community/docker-coq-action/issues/65 , and then we can update...
The build is quite noisy, filled with messages like ``` File "./theories/Categories/Functor/Composition/Laws.v", line 43, characters 0-55: Warning: The default value for hint locality is currently "local" in a section and...
The new build system fixed the per-file dependency graphs but broke the whole-library dependency graphs at, e.g., https://hott.github.io/HoTT/dependencies/HoTTCore.svg
Every time I build, I get errors such as ``` theories/Homotopy/ExactSequence.vo (real: 28.06, user: 26.58, sys: 1.23, mem: 597200 ko) HOQC theories/Spaces/No/Addition Fatal error: exception Stack overflow Error: Native compiler...