We have a FunExt interface containing general enough proposition, for omega-quantitied functions. But this property is also useful for functions taking arguments with the other quantities as well. Thankfully, these properties are derivable from the existing one, so I propose to add them with their proofs to the library.
Should this change go in the CHANGELOG?
[x] If this is a fix, user-facing change, a compiler change, or a new paper
implementation, I have updated CHANGELOG_NEXT.md (and potentially also
CONTRIBUTORS.md).
Description
We have a
FunExtinterface containing general enough proposition, for omega-quantitied functions. But this property is also useful for functions taking arguments with the other quantities as well. Thankfully, these properties are derivable from the existing one, so I propose to add them with their proofs to the library.Should this change go in the CHANGELOG?
CHANGELOG_NEXT.md(and potentially alsoCONTRIBUTORS.md).