[2019-08-12]
YOW! Lambda Jam 2019 - Philip Wadler: (Programming Languages) in Agda = Programming (Languages in Agda) /r/functionalprogramming [[towatch]] [[agda]][2018-10-10]
Agda Beginner(-ish) Tips, Tricks, & Pitfalls - Donnacha Oisín Kidney [[agda]][2019-04-21]
Cubical Agda and Probability Monads /r/agda [[agda]][2018-11-13]
good with explanation https://agda.readthedocs.io/en/latest/language/with-abstraction.html#simultaneous-abstraction [[agda]][2019-01-26]
agda-ring-solver https://oisdk.github.io/agda-ring-solver/README.html data _≡_ {A : Set} : A → A → Set where
refl : {a : A} → a ≡ a
sym : ∀ {A} {a b : A} → a ≡ b -> b ≡ a
sym refl = refl
data ℕ : Set where
Z : ℕ
S : ℕ → ℕ
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 ())
[2019-08-12]
YOW! Lambda Jam 2019 - Philip Wadler: (Programming Languages) in Agda = Programming (Languages in Agda) /r/functionalprogramming [[towatch]] [[agda]][2018-10-10]
Agda Beginner(-ish) Tips, Tricks, & Pitfalls - Donnacha Oisín Kidney [[agda]]https://doisinkidney.com/posts/2018-09-20-agda-tips.html
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]][2018-11-13]
good with explanation https://agda.readthedocs.io/en/latest/language/with-abstraction.html#simultaneous-abstraction tldr: write multiple with clauses; then pattern match on them to rewrite and eliminate
https://www.reddit.com/r/haskell/comments/a2d3pg/_/eax3ml7?context=1000
В Агдочку Prop'ов завезли! https://t.co/1s98uSyGd8
<https://twitter.com/deniok/status/1116737917421064192 >
[2018-11-11]
agda/Records.agda at master · agda/agdahttps://github.com/agda/agda/blob/master/examples/SummerSchool07/Lecture/Records.agda
[2018-11-11]
agda/Sigma.agda at master · agda/agdahttps://github.com/agda/agda/blob/master/src/data/lib/prim/Agda/Builtin/Sigma.agda
[2018-11-13]
Abstract Algebra in Agdahttps://people.inf.elte.hu/pgj/agda/tutorial/Application.Algebra.html
[2018-11-13]
With-Abstraction — Agda 2.6.0 documentationhttps://agda.readthedocs.io/en/latest/language/with-abstraction.html#simultaneous-abstraction
Rendering context...