Agda is a programming language created in 2007 by Ulf Norell and Catarina Coquand.
| #173on 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)
(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
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][\da-fA-F]+ |
|
| 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 |