finegeometer

Is there a workaround for this problem, if I want to run Agda code in the browser now?

Thank you! > Your program has one syntax error: `i32.MIN` should be `i32::MIN`. Not surprising, I retyped the program rather than copy-pasting. (I don't remember why.) So typos were likely....

So far, it hasn't been clear whether this "unintentional feature" is sound. If it isn't, I imagine the counterexample will be some variation of the following. ```agda open import Level...

Oops, I made a typo. That should have said `X : (ℓ : Level) → Set (suc ℓ)`. Anyway, my reasoning was as follows. - In a context with `x...

Looking back at this, I think my guesses are correct. In addition, I think the third number in the last field is the distance _across_ the transistor, from the source...

> Inconsistent behavior may make this issue hard to test, and also hard to track down. The inconsistency here is whether 16 or 17 long bars make it to the...

I think I've tracked down the issue. On my Firefox installation, `KeyboardEvent.repeat` always returns false, even when it should return true. As a result, the function `handleTappedDirection` in `input_manager.js` is...

Something just occurred to me: If you want the theorem to compute efficiently, it should probably be reimplemented using the [union-find algorithm](https://en.wikipedia.org/wiki/Disjoint-set_data_structure). Computational behavior wasn't a concern for my application,...

Why not `compare : ∀ x y → (x ≤ y) ∗ (y ≤ x)`, where `_∗_` is as defined in `Homotopy.Join`? This is equivalent to `∥ (x ≤ y)...

Just as a datapoint, I find this merging of imports to be sufficient reason to disable `elm-format`, when I would otherwise use it. I find it actively misleading to have...