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){-# OPTIONS --cubical --safe #-}
module Test where
open import Cubical.Core.Everything
open import Cubical.Relation.Nullary
open import Cubical.Data.Fin
import Pig using (pig)
check : ∀ {n} {m} → ¬ (n ≡ m) → ¬ (Fin n ≡ Fin m)
check = Pig.pigFundamentals
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)
}