Agda
Table of Contents
- Propositional equality agda
- Natural numbers agda
- Finite type agda
- TODO [D] YOW! Lambda Jam 2019 - Philip Wadler: (Programming Languages) in Agda = Programming (Languages in Agda) /r/functionalprogramming agdatowatch
- [D] Agda Beginner(-ish) Tips, Tricks, & Pitfalls - Donnacha Oisín Kidney agda
- TODO [D] A Few Haskell Highlights: Top Haskell Resources of 2019 agda
- Cubical Agda and Probability Monads /r/agda agda
- good with explanation https://agda.readthedocs.io/en/latest/language/with-abstraction.html#simultaneous-abstraction agda
- TODO [D] https://math.stackexchange.com/a/1307770/15108 prove isomorphism? agdatostudy
- TODO [D] Philip Wadler and Wen Kokke publish book on Programming Language Foundations in Agda agda
- TODO [D] Tweet from Denis Moskvin (@deniok), at Apr 12, 17:20 agda
- [D] Agda stuff agda
- [D] agda-ring-solver https://oisdk.github.io/agda-ring-solver/README.html agda
¶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] YOW! Lambda Jam 2019 - Philip Wadler: (Programming Languages) in Agda = Programming (Languages in Agda) /r/functionalprogramming agdatowatch
¶[D] Agda Beginner(-ish) Tips, Tricks, & Pitfalls - Donnacha Oisín Kidney agda
¶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.
¶ Cubical Agda and Probability Monads /r/agda agda
¶ good with explanation https://agda.readthedocs.io/en/latest/language/with-abstraction.html#simultaneous-abstraction 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]
https://www.reddit.com/r/haskell/comments/a2d3pg/_/eax3ml7?context=1000
¶TODO [D] Tweet from Denis Moskvin (@deniok), at Apr 12, 17:20 agda
CREATED: [2019-04-12]
В Агдочку Prop'ов завезли! https://t.co/1s98uSyGd8