Ad

Show that if n ≡ m is not true, then Fin n ≡ Fin m is not true.

{-# OPTIONS --cubical --safe #-}

module Pig where
open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
open import Cubical.Relation.Nullary
open import Cubical.Data.Fin
open import Cubical.Data.Empty

pig : ∀ {n} {m} → ¬ (n ≡ m) → ¬ (Fin n ≡ Fin m)
pig nm p = nm (Fin-inj p)
Fundamentals
Lists
Data Structures
Functional Programming
Declarative Programming
Programming Paradigms

That's good

/**
 * Created by ice1000 on 2017/4/27.
 *
 * @author ice1000
 */

fun <A, B, C : Any> zipWith(op: (A, B) -> C) = { x: Sequence<A> ->
	{ y: Sequence<B> ->
		val iX = x.iterator()
		val iY = y.iterator()
		generateSequence {
			if (iX.hasNext() and iY.hasNext()) op(iX.next(), iY.next())
			else null
		}
	}
}

fun <T : Any> generate() = zipWith { x: Int, y: T -> "[$y * x^$x]" } (
	generateSequence(0, Int::inc)
)

fun main(args: Array<String>) =
		generate<Int>()(sequenceOf(1, 1, 2, 3, 5, 8, 13, 21)).forEach(::println)
Fundamentals
Lambdas
Functional Programming
Functions
Declarative Programming
Programming Paradigms
Control Flow
Basic Language Features

Lambda recursion.

/**
 * Created by ice1000 on 2017/5/2.
 *
 * @author ice1000
 */
fun main(args: Array<String>) {
	fun lambda(it: Int): Int =
			if (it <= 2) 1 else lambda(it - 1) + lambda(it - 2)
	(1..10).map(::lambda) // .forEach(::println)

	var lambda2: (Int) -> Int = { it }
	lambda2(1)
	lambda2 = { if (it <= 2) 1 else lambda(it - 1) + lambda(it - 2) }
	(1..10).map(lambda2) // .forEach(::println)
}