Add CLog with well-defined zero case #57
Draft
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The PR adds the
CLogWZ
type family to the solver, which allows for aCLog
definition with a well defined output for the case of the second non-base argument being zero. In this case the third argument is returned instead. The type family can be useful in cases, where the zero case needs to defined, as for example in theIndex 0
case withinclash-prelude
(cf. clash-compiler PR #2784).Reviewers Note
The currently used naming scheme might still be a bit adhoc, but I couldn't figure out any more elegant solution yet. One option might be to add total versions for all non-total type families of
ghc-typelits-extra
with extra parameters defining the return value in the undefined cases. In terms of naming we then just could addTotal
as a prefix / suffix to these versions, e.g.,TotalDiv
orDivTotal
. In the particular case ofCLog
there are many undefined cases, however, which makes me unsure of how practical this approach would be.TODOs