# Agda

Agda is an actively used programming language created in 2007. Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The current version of Agda was originally known as Agda 2. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. Read more on Wikipedia...

12Years Old | 25Users | 0Jobs |

- Agda ranks in the top 10% of languages
- the Agda website
- the Agda wikipedia page
- Agda first appeared in 2007
- file extensions for Agda include agda
- tryitonline has an online Agda repl
- See also: coq, epigram, haskell, idris, emacs-editor, unicode, javascript
- I have 55 facts about Agda. what would you like to know? email me and let me know how I can help.

### Example code from Linguist:

module NatCat where open import Relation.Binary.PropositionalEquality -- If you can show that a relation only ever has one inhabitant -- you get the category laws for free module EasyCategory (obj : Set) (_⟶_ : obj → obj → Set) (_∘_ : ∀ {x y z} → x ⟶ y → y ⟶ z → x ⟶ z) (id : ∀ x → x ⟶ x) (single-inhabitant : (x y : obj) (r s : x ⟶ y) → r ≡ s) where idʳ : ∀ x y (r : x ⟶ y) → r ∘ id y ≡ r idʳ x y r = single-inhabitant x y (r ∘ id y) r idˡ : ∀ x y (r : x ⟶ y) → id x ∘ r ≡ r idˡ x y r = single-inhabitant x y (id x ∘ r) r ∘-assoc : ∀ w x y z (r : w ⟶ x) (s : x ⟶ y) (t : y ⟶ z) → (r ∘ s) ∘ t ≡ r ∘ (s ∘ t) ∘-assoc w x y z r s t = single-inhabitant w z ((r ∘ s) ∘ t) (r ∘ (s ∘ t)) open import Data.Nat same : (x y : ℕ) (r s : x ≤ y) → r ≡ s same .0 y z≤n z≤n = refl same .(suc m) .(suc n) (s≤s {m} {n} r) (s≤s s) = cong s≤s (same m n r s) ≤-trans : ∀ x y z → x ≤ y → y ≤ z → x ≤ z ≤-trans .0 y z z≤n s = z≤n ≤-trans .(suc m) .(suc n) .(suc n₁) (s≤s {m} {n} r) (s≤s {.n} {n₁} s) = s≤s (≤-trans m n n₁ r s) ≤-refl : ∀ x → x ≤ x ≤-refl zero = z≤n ≤-refl (suc x) = s≤s (≤-refl x) module Nat-EasyCategory = EasyCategory ℕ _≤_ (λ {x}{y}{z} → ≤-trans x y z) ≤-refl same

### Example code from Wikipedia:

data _≤_ : ℕ → ℕ → Set where z≤n : {n : ℕ} → zero ≤ n s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m

Last updated August 22nd, 2019