porglezomp

-- Note: There is a more complete explanation at https://github.com/hwayne/lets-prove-leftpad/tree/master/idris
import Data.Vect

-- `minus` is saturating subtraction, so this works like we want it to
eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k
eq_max  n     Z    = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl
eq_max  Z    (S _) = Refl
eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl

-- The type here says "the result is" padded to (maximum k n), and is padding plus the original

monzee

import kotlin.coroutines.experimental.*

fun main(vararg args: String) {
    safeDiv(None(), Some(1)).let(::println)
    safeDiv(Some(5L), Some(0.5)).let(::println)
    safeDiv(Some(1), None()).let(::println)

    for (x in 20..30 step 5) {
        for (y in 15 downTo 0 step 5) {
            print("$x / $y = ")