Rob Lewis

I'll double check this next time I'm at my office computer, but I'm fairly sure the issues I've had with wildcard behavior follow the same pattern as @theemathas' example. When...

Here's another example using wildcards that fails unexpectedly, or at least it's unexpected given my intuitions about wildcards. I don't know how related this is to the above problems. If...

Oh, I see, the PR to a branch tripped me up -- sorry! "mental parse error" is a great way to describe how I feel about `triangle_free_far` :grin:

I think quite a few of the `expr` functions have this unnecessary restriction and should be generalized. But it takes someone knowledgeable to know which are which, or to carefully...

That's fair, and probably the less disruptive way to do this!

Thanks! The description on the website you link to says that the course will use Haskell and Coq; is this outdated? Are there any public materials for your course you're...

Are we using this feature at all? It looks like all our jinja2 templates are .html files, but I'm not sure. Also I have no idea how to disable this...

I agree with Mario. Note that `#check module_ext` prints the same. The docs aren't generated from the input files (nor should they be), they're generated from the compiled library by...

I don't think it's an issue. The pretty printer is doing what it's supposed to. Both of those terms are `r • m` (with different implicit arguments), what do you...

> I might not know what I am talking about, but it might be possible to perform some kind of binary search on the exponent in the range of say...