Jacques Carette
Jacques Carette
See PR #2652 . I think @jamesmckinna had already started down this road, this is continuing that. But I want to make sure that this is the design we want...
Issue #2532 from @jamesmckinna draws our attention to some of the left/right inconsistencies. There are... more. I attach two lists (courtesy of @jmougeot ), one which details definitions that use...
A quite thorough description of the issue is [already written](https://github.com/agda/agda/pull/7728#issuecomment-2695418542) so I won't repeat it all here. Basically some of our `NonZero` instances resolve through sheer luck of the details...
For example, is [this file](https://github.com/agda/agda-stdlib/blob/master/tests/reflection/assumption/Main.agda) actually used? It appears that these lines https://github.com/agda/agda-stdlib/blob/94906c00c9b0afab2283149fa33875e31b226a61/tests/reflection/assumption/Main.agda#L54-L58 are wrong and instead should be printed "in context" which `concatMap` doesn't do. The original report (on...
In #2545 @jamesmckinna mentions > most recent (knock-on) commit exposes a slight wrinkle in the parameterization: use here of the lemma, instantiated to Setoid S arises there as (S Membershipₚ.∉[])...
This issue is a place to discuss the design of what we'd like. @jamesmckinna gave a first PR (#1962 ) that has been long stalled (because of, well, me!) So...
Glassbr for `LR`: ``` ** \brief Calculates load resistance: the uniform lateral load that a glass construction can sustain based upon a given probability of breakage and load duration as...
Example: ``` /** \brief Calculates Process Variable: The output value from the power plant ``` Feels like the "Process Variable" is overly abstract, coming from the model, rather than being...
Most of the code comments we previous had were ridiculously redundant. PR #4298 got rid of that. Unfortunately some useful information got lost at the same time -- but much...
In glassbr, q has as comment ``` \brief Calculates applied load (demand): 3 second duration equivalent pressure (Pa) ``` The term "applied load (demand)" is indeed quite different from "3...