Add inference for #917 #927
Conversation
Codecov Report
@@ Coverage Diff @@
## master #927 +/- ##
==========================================
+ Coverage 91.63% 91.75% +0.12%
==========================================
Files 49 49
Lines 538 546 +8
Branches 12 5 -7
==========================================
+ Hits 493 501 +8
Misses 45 45
Continue to review full report at Codecov.
|
| @@ -5,6 +5,8 @@ import eu.timepit.refined.api.Inference | |||
| import eu.timepit.refined.boolean._ | |||
There was a problem hiding this comment.
I'm kinda worried that this file is only in scala-3.0- 🤔
modules/core/shared/src/main/scala-3.0-/eu/timepit/refined/boolean.scala
Outdated
Show resolved
Hide resolved
| p1: B ==> C, | ||
| p2: A ==> C | ||
| ): (A Or B) ==> C = | ||
| Inference.combine(p1, p2, "disjunctionElimination") |
There was a problem hiding this comment.
Combine is "and", did you mean to make this use "or"? (as we discussed, probably rqeuires a new method)
There was a problem hiding this comment.
Yep, but we were wrong :) In order to imply that A Or B can be replaced by C, both A and C needs to be equivalents of C.
Here is the truth table for OR option:
A B C │ ((B ↔ C) ∨ (A ↔ C)) → ((A ∨ B) ↔ C)
───────┼─────────────────────────────────────
1 1 1 │ 1 1 1 *1 1 1
1 1 0 │ 0 0 0 *1 1 0
1 0 1 │ 0 1 1 *1 1 1
1 0 0 │ 1 1 0 *0 1 0
0 1 1 │ 1 1 0 *1 1 1
0 1 0 │ 0 1 1 *0 1 0
0 0 1 │ 0 0 0 *1 0 0
0 0 0 │ 1 1 1 *1 0 1
|
@fthomas could you review this please? |
Agreed with @kubukoz that this PR will replace his #919.
I've suggested some naming, made one of inferences more generic, and added scala 3.0+ version.