porglezomp

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
leftPad : (x : a) -> (n : Nat) -> (xs : Vect k a)

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 = ")