| {-# OPTIONS --without-K #-} | |
| module C where | |
| open import Function | |
| open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; trans; cong; sym) | |
| open import Data.Empty | |
| open import Data.Bool | |
| open import Data.Product as Prod using (∃-syntax; Σ-syntax; _,_; _×_; ∃; proj₁; proj₂) | |
| open import Data.Maybe as Maybe using (Maybe; just; nothing; is-just) | |
| open import Data.Sum as Sum using (_⊎_; inj₁; inj₂) |
| ### Keybase proof | |
| I hereby claim: | |
| * I am winitzki on github. | |
| * I am winitzki (https://keybase.io/winitzki) on keybase. | |
| * I have a public key ASCGlyC2foE8dsomD34cEbdGXNtkOVwUbyRSnQ3vwSV_Igo | |
| To claim this, I am signing this object: |
Copyright © 2016-2017 Fantasyland Institute of Learning. All rights reserved.
A function is a mapping from one set, called a domain, to another set, called the codomain. A function associates every element in the domain with exactly one element in the codomain. In Scala, both domain and codomain are types.
val square : Int => Int = x => x * x