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 ())
```

¶[D][2018-10-10] Agda Beginner(-ish) Tips, Tricks, & Pitfalls - Donnacha Oisín Kidney agda

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

¶[2019-04-21]Cubical Agda and Probability Monads /r/agda agda

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
```