Jacques Carette
Jacques Carette
I don't think we should have a single list. The meaning of "input constraints" and "problem constraints" are different (even though the input constraints are a subset of the problem...
What currently exists is indeed multiple (two) lists, but whose meaning is muddled. I'm suggesting multiple lists but where each has a clearer meaning, and thus their names could then...
Yes - but let's try to analyze our requirements before we jump to solutions. Spell out what you see as the 'real' problem, and then we can explore the space...
What's the current CSS that regulates this? We're so far from being mobile-ready, I think it's fine to ignore that for now.
I put it in v2.2 as I really would like to push this through.
We've decided to close this for now, in favour of the "project issue #2511 " as it's a bigger deal.
While I'm generally in favour, I'd also like to know: what function is responsible for introducing the `trans refl`? It feels like it's the "guilty party" here and should be...
I agree that this is likely not the only instance (there are tons of similar things in `agda-categories` but their 'source' is more complex due to "bad" definitions in category...
As a sanity check, sure. As a way to build the library via meta-programming? Maybe. As a way to *build* the library? Definitely not!
Right, if our combinators built up a list of steps, and then either `begin_` or `_∎` turned that into an actual proof, we could optimize. I can see if one...