Agda is a programming language created in 2007 by Ulf Norell and Catarina Coquand.
#175on PLDB  16Years Old  731Users 
7Books  14Papers  2kRepos 
Try now: TIO
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...
module agda where
open import IO
main = run (putStrLn "Hello World")
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)
(singleinhabitant : (x y : obj) (r s : x ⟶ y) → r ≡ s)
where
idʳ : ∀ x y (r : x ⟶ y) → r ∘ id y ≡ r
idʳ x y r = singleinhabitant x y (r ∘ id y) r
idˡ : ∀ x y (r : x ⟶ y) → id x ∘ r ≡ r
idˡ x y r = singleinhabitant 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 = singleinhabitant 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 NatEasyCategory = EasyCategory ℕ _≤_ (λ {x}{y}{z} → ≤trans x y z) ≤refl same
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m
Feature  Supported  Token  Example 

MultiLine Comments  ✓  
Integers  ✓   \d+ 

Floats  ✓   \d+[eE][+]?\d+ 

Hexadecimals  ✓   0[xX][\dafAF]+ 

Strings  ✓  "  "Hello world" 
Print() Debugging  ✓  putStrLn  
Comments  ✓   A comment 

Line Comments  ✓     A comment 
Typed Holes  ✓  
Semantic Indentation  X 
title  author  year  reviews  ratings  rating 

Verified Functional Programming in Agda  Aaron Stump  0  1  4.00  
Verified Functional Programming in Agda  Aaron Stump  0  0  0.0  
Programming Language Foundations in Agda  Philip Wadler  0  0  0.0 
title  authors  year  publisher 

Verified Functional Programming in Agda (ACM Books)  Stump, Aaron  2016  ACM Books 
Verified Functional Programming in Agda (ACM Books)  Stump, Aaron  2016  ACM Books 
Verified Functional Programming in Agda  Aaron Stump  20160201  Morgan & Claypool Publishers 
Verified Functional Programming in Agda  Aaron Stump  20160201  Morgan & Claypool Publishers 