tschuchort
11/20/2019, 12:07 PMImran/Malic
11/20/2019, 12:08 PMtype-proofs
are global not like the one Scala
hastschuchort
11/20/2019, 12:09 PMImran/Malic
11/20/2019, 12:13 PMtschuchort
11/20/2019, 12:20 PMfun p1(from: Int): Long = (from as Long)
and
fun p2(from: Int): Long = (-from as Long)
They are both proofs of the same proposition but at the end of the day the conversion is different.fun <A,B> unsound(from: A): B = Nothing
that is a proof of every proposition.Imran/Malic
11/20/2019, 12:26 PMfrom
and to
are properties. you would do something like:
fun Int.from1(): Long = ...
fun Long.to1(): Int = ...
fun Int.from2(): Long = ...
fun Long.to2(): Long = ...
Jannis
11/20/2019, 12:26 PMImran/Malic
11/20/2019, 12:30 PMJannis
11/20/2019, 12:31 PMraulraja
11/20/2019, 12:38 PM