Harrison Grodin

However, we now have: https://github.com/jonsterling/cost-refinement-lab/blob/ffad8eafec348a9a890723e35faf9d02ff0a8db4/src/Calf/Types/Eq.agda#L17-L18 Although, it's only used here: https://github.com/jonsterling/cost-refinement-lab/blob/ffad8eafec348a9a890723e35faf9d02ff0a8db4/src/Calf/Noninterference.agda#L22 (Perhaps `Noninterference` should be with K, and `eq/uni` should be defined using `uip` rather than postulated? Not sure.)

Do we want to put these in before submission, or leave as-is (some files with, some without)?

This seems like a great feature to have. The less magic, the better, since Rewrite aims to work with generic rules. It seems like the following should solve everything but...

**TL;DR:** Distributivity is hard, and applying it well in practice is somewhat unclear. It's a difficult problem to tackle, but a medium-term `#TODO`. --- Dealing with distributivity is a tough...

The subjectivity is only the reason why we don't (currently) include any mention of the distributive law in the standard rule set. If the expanded form is okay, though, I...

I would absolutely agree that all imprecision with floating point calculations should be considered more of a bug than a feature. ```julia julia> f(x) = sin(x)^2 + cos(x)^2; # expected:...

Ah, fantastic! Glad there's a precedence for that. I'd rather not fall back to any floating-point arithmetic, since that's accepting an approximation; instead, it seems more pure to just retain...

According to some very unscientific testing, current change cuts speed (and allocations) down by a factor of around 2. Still a couple of seconds on a fast machine to run...

From what I understood, #38 was meant to be about the speed of initially creating the rule set (by calling `rules()`), which is currently unreasonably slow the first time due...

```julia julia> using Rewrite julia> @time rules(); 2.365382 seconds (3.59 M allocations: 179.190 MiB, 3.12% gc time) julia> @time rules(); 0.017669 seconds (21.51 k allocations: 1007.078 KiB) ``` Seems like...