Víctor López Juan

@Saizan pointed out that, if there happens to be more than one error in a failing block, which one will trigger is unspecified. On the other hand, the different phases...

We had a meeting today. Here are some things that should be fixed before merging. - [ ] `AlwaysUnblock` should not be used as a synonym for `True` in `runPureConversion`....

Have you tried using stack? I can build it with all the stack files in the repo, and the test suite passes at least when built with stack-8.10.3.yaml.

> I have trouble building the code ([1309bdb](https://github.com/agda/agda/commit/1309bdb41cc6cc9066f93bd5cc51cf9dfec7c236)). I have repeatedly encountered the following internal error (on a 32-bit system): > > ``` > [346 of 400] Compiling Agda.TypeChecking.Rules.LHS (...

@nad You can try the version of the standard library that this version of Agda is built against: https://github.com/agda/agda-stdlib/commit/d00ba75

For the record, the regression was introduced from d41a104958c531 to 88e00e048a8ee0 . The crux of the issue lies in the following two constraints: > elim _P_121 _r_122 (refl _x_120) =...

> That might be annoying, I encountered unsolved metavariables for a number of pieces of similar-looking code. One possibility is to add a flag which, using the new constraint prioritization...

> @vlopezj, how would Tog handle this situation? @nad The blocking mechanism in Tog is the same as Ulf describes, so you could have the same issues there.

FWIW, as a workaround, you can: 1. Export the event (by clicking the memory-card shaped icon) 2. Browse to the exported file, and import the event into the appropriate calendar....

How about `whileRight` or `untilLeft`? Either standalone, or prefixed with `run`, `runIter` or `iter`. The `probability` package uses `untilLeft` [1]. According to Google, the other alternatives are not used by...