[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...