Thomas Lamiaux

Module and elim

1

@felixwellen realized last week that there is files such as the [Free comMonoid](https://github.com/agda/cubical/blob/master/Cubical/HITs/FreeComMonoids/Base.agda) or [Direct Sum](https://github.com/agda/cubical/blob/master/Cubical/Algebra/DirectSum/Base.agda) that define a named module with one function f. So one need to call...

Usually in the addition on something is defined on the left, plus in some case this is the only possible way. However, the addition on the integer is defined on...

I have found at least two examples where it returns the anomaly "List.chop" when something is not fully applied A minimal example where not all variables have been given: ```...

Z3 does not build by default on ubuntu 24.04

3

I tried to install z3 with opam on ubuntu 24.04, which fails with the following error message ``` opam install z3.4.13.0 [ERROR] Package z3.4.13.0 depends on the unavailable system package...

A Compilation of Short Interactive Tutorials and How-To Guides for Coq

4

Hi, it took a lot of effort to write, hope you think it is good. [Rendered](https://github.com/thomas-lamiaux/ceps/blob/master/text/XXX-A-Compilation-of-Short-Interactive-Tutorials-and-How-To-Guides-for-Coq.md)

Towards a common done tactic

6

Benchmarking a new version of done linked to this discussion https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Towards.20a.20common.20done

Checking can "work" even if parsing fails

2

``` Goal forall {P }, P -> 0 = 0. contr Lemma foo : 0 = 0. intros. ``` 

There is currently a button to close the proof view but it reopens constantly at each interaction which is not always wanted as some users: - don't need it for...

Parsing issues with MetaCoq

3

At the moment, basically all the files in https://github.com/thomas-lamiaux/generating_recursors creates parsing issue. I can not exactly isolate a file as it happens from time to time when I open files....

Hi, would it possible be to have a small option to set the default size of the proof window ? I don't know how it works currently, but it often...