These are chat archives for fthomas/refined

5th
Jun 2018
Gastón Tonietti
@ktonga
Jun 05 05:19
quick question, can't I use predicates such as Greater with scala.math.BigDecimal? seems that if i only use Positive it works but when i include a predicate with witness it stops working, or maybe i dont know how a BD literal looks like
Howy Perrin
@howyp
Jun 05 06:03
Whoops. If I remember correctly you can't witness on a BigDecimal. But if Positive works, then Greater should work too if you can express the argument to Greater as a Nat. Greater[_5]
Gastón Tonietti
@ktonga
Jun 05 06:55
will try it later. thank you @howyp
Frank S. Thomas
@fthomas
Jun 05 08:44
@howyp I've seen this IntelliJ problem too, IIRC it occurs since the last Scala Native update. But I've no idea how to fix that
Howy Perrin
@howyp
Jun 05 08:44
😞 ok, thanks - at least it’s not just me.
out of curiosity, what do you use? Ensime?
Julien Truffaut
@julien-truffaut
Jun 05 08:52
is it possible to prove that P1 => P2, e.g. Int Refined Greater[_10] => Int Refined Positive
Frank S. Thomas
@fthomas
Jun 05 09:27
@julien-truffaut yes, there is an implicit conversion macro in auto._ which can do this:
scala> val x: Int Refined Greater[_10] = 20
x: Refined[Int, Greater[_10]] = 20

scala> val y: Int Refined Positive = x
y: Refined[Int, Positive] = 20
@howyp I'm using IntelliJ
Julien Truffaut
@julien-truffaut
Jun 05 09:28
awesome, thanks. Does it work even when x is not a literal?
Frank S. Thomas
@fthomas
Jun 05 09:30
yes, the macro only looks at the types of x and y
Julien Truffaut
@julien-truffaut
Jun 05 09:31
great
Howy Perrin
@howyp
Jun 05 09:52
@fthomas so how do you get the project to import? 🤔
Frank S. Thomas
@fthomas
Jun 05 10:31
:hear_no_evil: :see_no_evil:
Howy Perrin
@howyp
Jun 05 12:58
🤣