agda

# Agda

[2013-09-24]

## ¶Propositional equality agda

```data _≡_ {A : Set} : A → A → Set where
refl : {a : A} → a ≡ a

sym : ∀ {A} {a b : A} → a ≡ b -> b ≡ a
sym refl = refl
```

## ¶Natural numbers agda

```data ℕ : Set where
Z : ℕ
S : ℕ → ℕ
```

## ¶Finite type agda

```data Fin : ℕ → Set where
fzero : (n : ℕ) -> Fin (S n)
fsucc : (n : ℕ) -> Fin n -> Fin (S n)

onlyone : (x : Fin (S Z)) → x ≡ fzero Z
onlyone (fzero .Z) = refl
onlyone (fsucc .Z ())
```

## ¶TODO[D] A Few Haskell Highlights: Top Haskell Resources of 2019 agda

CREATED: [2019-12-27]
```To get to know Agda better, you can read this introductory post by Danya Rogozin.
```

## ¶[2018-11-13] good with explanation https://agda.readthedocs.io/en/latest/language/with-abstraction.html#simultaneous-abstractionagda

tldr: write multiple with clauses; then pattern match on them to rewrite and eliminate

## ¶TODO[D]https://math.stackexchange.com/a/1307770/15108 prove isomorphism? agdatostudy

CREATED: [2018-11-14]

## ¶TODO[D] Philip Wadler and Wen Kokke publish book on Programming Language Foundations in Agda agda

CREATED: [2019-01-01]

## ¶TODO[D] Tweet from Denis Moskvin (@deniok), at Apr 12, 17:20 agda

CREATED: [2019-04-12]
```В Агдочку Prop'ов завезли! https://t.co/1s98uSyGd8
```