Jacques Carette
Jacques Carette
Yes, please make #3858 close this issue.
- percent in italics should be made into a separate issue. It's likely bound up with other issues, so that changing that might not be so easy - hopefully you've...
Up to @balacij to verify that the changes he'd asked for have been done.
Indeed things have further evolved. So I think this might even have already been done, and the new thing is `Concept` (though it might not have been fully implemented). What's...
If our names are too short and causing conflicts, we can lengthen them. We can also move to using more qualified names, which is probably a better way to deal...
The problem is that this `g` comes out of nowhere. So yes, a solution can be arbitrary-valued outside the scope. It feels like maybe the right way to do that...
That's an extensionality property - you're asking for a pointwise proof to 'upgrade' to a uniform proof.
If you represent `f` and `g` as `Vec`, so that the finiteness is apparent, instead of being hidden under a function, then it is provable.
Thanks a lot for the report - one of us will look in more detail soon.
Ack. that this is on my plate.