| {-# 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₂) |
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