Agda
1 program
Added 2025-10-22T15:12:35Z
Model: anthropic/claude-4.5-sonnetTemp: 0.4
Evidence
Report issue
View issues
Aliases: agda
Provenance: commit 19ea5c31fe · authored 2025-10-22T17:12:35+02:00 · model anthropic/claude-4.5-sonnet
Sources mentioning this language
8 sources · pl_id:
pl/agdaWikipedia infobox ↗
Pulled from the
wikimedia/structured-wikipedia
snapshot — see data/raw/wikipedia_pl_facts.*.jsonl and
pl_fact.csv for the long-table provenance.
| Paradigms | total functional |
|---|---|
| Typing | strong, static, dependent, nominal, manifest, inferred |
| Designed by | Chalmers University of Technology · Ulf Norell · Catarina Coquand (1.0) |
| First appeared | 1999 |
| Influenced by | Rocq · Epigram · Haskell |
| License | BSD-like |
| Implemented in | Haskell |
| Homepage | https://wiki.portal.chalmers.se/agda |
Extensions claimed by this language
4 claims. Each row is one upstream assertion with its strength.
SWH column shows file occurrences with that extension across the entire archive.| Extension | Source | Strength | SWH |
|---|---|---|---|
.agda | linguist | primary | 354.3K files |
.agda | pygments | primary | 354.3K files |
.agda | wikidata | primary | 354.3K files |
.lagda | wikidata | primary | 60.5K files |
Related languages
LLM-contributed programs
Natural Number Addition Proof
Provenance: commit 19ea5c31fe · authored 2025-10-22T17:12:35+02:00 · model anthropic/claude-4.5-sonnet · Temp 0.4
module Nat where
data Nat : Set where
zero : Nat
suc : Nat → Nat
{-# BUILTIN NATURAL Nat #-}
infixl 6 _+_
_+_ : Nat → Nat → Nat
zero + m = m
suc n + m = suc (n + m)
infixl 7 _*_
_*_ : Nat → Nat → Nat
zero * m = zero
suc n * m = m + n * m
infixl 6 _∸_
_∸_ : Nat → Nat → Nat
m ∸ zero = m
zero ∸ suc n = zero
suc m ∸ suc n = m ∸ n
data _≤_ : Nat → Nat → Set where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
infix 4 _≤_
≤-refl : ∀ {n} → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl
≤-trans : ∀ {l m n} → l ≤ m → m ≤ n → l ≤ n
≤-trans z≤n _ = z≤n
≤-trans (s≤s l≤m) (s≤s m≤n) = s≤s (≤-trans l≤m m≤n)
≤-antisym : ∀ {m n} → m ≤ n → n ≤ m → m ≡ n
≤-antisym z≤n z≤n = refl
≤-antisym (s≤s m≤n) (s≤s n≤m) = cong suc (≤-antisym m≤n n≤m)
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
infix 4 _≡_
{-# BUILTIN EQUALITY _≡_ #-}
sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl
trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl
cong : ∀ {A B : Set} (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl
+-assoc : ∀ m n p → (m + n) + p ≡ m + (n + p)
+-assoc zero n p = refl
+-assoc (suc m) n p = cong suc (+-assoc m n p)
+-identity : ∀ n → n + zero ≡ n
+-identity zero = refl
+-identity (suc n) = cong suc (+-identity n)
+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc zero n = refl
+-suc (suc m) n = cong suc (+-suc m n)
+-comm : ∀ m n → m + n ≡ n + m
+-comm m zero = +-identity m
+-comm m (suc n) = trans (+-suc m n) (cong suc (+-comm m n))Real programs from Software Heritage
No SWH evidence indexed yet for this language. (Either the SWH mining hasn't reached this language's extensions, or no matching files exist in the archive.)