Failed Tests

### Finite sets of different cardinalities are different

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)``````
Failed Tests

### Kotlin can have point free too!

Fundamentals
Lists
Data Structures
Functional Programming
Declarative Programming

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)``````
Failed Tests

### Kotlin lambda recursion

Fundamentals
Lambdas
Functional Programming
Functions
Declarative Programming
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)
}``````