Cass Alexandru<p>So I have this exact problem with the <a href="https://types.pl/tags/emacs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>emacs</span></a> <a href="https://types.pl/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> input method (which has no answer and I'm wondering if it's because something in my config breaks quail somehow?) <a href="https://stackoverflow.com/questions/25319154/emacs-quail-input-method-how-to-complete-a-key-sequence" rel="nofollow noopener" target="_blank">emacs quail input method - how to complete a key sequence - Stack Overflow</a> Does anyone else have this? Quick check is to set <code>input-method</code> to <code>Agda</code>, then type <code>\set</code>. Then the only possible completion is <code>\setminus</code>, but I <u>have</u> to type the whole thing out…</p>
mastodon.world is one of the many independent Mastodon servers you can use to participate in the fediverse.
Generic Mastodon server for anyone to use.
Administered by:
Server stats:
8.2Kactive users
mastodon.world: About · Status · Profiles directory · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.4.0
#agda
0 posts · 0 participants · 0 posts today
José A. Alonso<p>Readings shared July 3, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/04-readings_shared_07-03-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/07/04-readings_shared_07-03-25</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a></p>
lxsameer<p>I like <a href="https://mastodon.social/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> as a language, but to be fair, its ecosystem and tooling are “crappy” at best. <br>Library management in agda is so bad, makes your eyes hurt.</p>
Cass Alexandru<p>I seem to remember some compiled-to-html output of proof scripts (could have been either <a href="https://types.pl/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a>, <a href="https://types.pl/tags/Isabelle" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Isabelle</span></a> or <a href="https://types.pl/tags/Lean" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean</span></a>, but maybe also a different proof assistant) which let you see the type of subterms on hover. Does this ring a bell w anyone? (I certainly wish we had sth like this for <a href="https://types.pl/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a>, my current approach is to replace the respective term w a hole and then reload the file and `C-c C-d` which is obviously not static, not to mention computationally expensive…)</p>
Programming Languages Delft<p>Master thesis by Maria Khakimova: "Enhancing Proof Assistant Error Messages with Hints: A User Study"</p><p>"We implemented hint enhancements for the error messages displayed upon three common mistakes: forgetting whitespace, using confusable Unicode characters, and supplying too few arguments to a function. A between-participants user study was then conducted with 70 students [..]"</p><p><a href="https://repository.tudelft.nl/record/uuid:52513287-7149-41f1-a8e8-8e38696cb283" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">repository.tudelft.nl/record/u</span><span class="invisible">uid:52513287-7149-41f1-a8e8-8e38696cb283</span></a></p><p><a href="https://akademienl.social/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://akademienl.social/tags/DependentTypes" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>DependentTypes</span></a> <a href="https://akademienl.social/tags/ProofAssistants" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ProofAssistants</span></a> <a href="https://akademienl.social/tags/ErrorMessages" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ErrorMessages</span></a> <a href="https://akademienl.social/tags/Usability" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Usability</span></a> <a href="https://akademienl.social/tags/UserStudy" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>UserStudy</span></a> <a href="https://akademienl.social/tags/master" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>master</span></a> <a href="https://akademienl.social/tags/thesis" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>thesis</span></a></p>
David C. Norris 🇺🇦<p>Extremely helpful exposition of Fin here by <span class="h-card" translate="no"><a href="https://agda.club/users/jesper" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>jesper</span></a></span> <a href="https://github.com/jespercockx/agda-lecture-notes/blob/master/agda.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">github.com/jespercockx/agda-le</span><span class="invisible">cture-notes/blob/master/agda.pdf</span></a>. At long last, it feels as if I'm on the cusp of 'getting' <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> ...</p>
Volker Stolz<p>Phil Wadler will talk online in 15 mins (if I got the timezone right) on "Lambda, the Ultimate Teaching Assistant (Agda version)":</p><p><a href="https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">fme-teaching.github.io/2021/08</span><span class="invisible">/24/tutorial-series-of-the-fme-teaching-committee/</span></a></p><p><a href="https://mastodon.social/tags/agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>agda</span></a> <a href="https://mastodon.social/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalMethods</span></a></p>
Jesper Agdakx 🔸I'm happy to inform you that as of Saturday, the <a class="hashtag" href="https://agda.club/tag/agda" rel="nofollow noopener" target="_blank">#Agda</a> documentation includes an explanation of the esoteric and obscure feature known as "lambda expressions": <a href="https://agda.readthedocs.io/en/latest/language/lambda-abstraction.html" rel="nofollow noopener" target="_blank">agda.readthedocs.io/en/latest/language/lambda-abstraction.html</a><br><br>(The old version only had pattern-matching lambdas.)
José A. Alonso<p>Readings shared May 31, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/31-readings_shared_05-31-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/05/31-readings_shared_05-31-25</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HoTT</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Minlog" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Minlog</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a></p>
José A. Alonso<p>Verifying Z3 RUP proofs with the interactive theorem provers Coq/Rocq and Agda. ~ Harry Bryant et als. <a href="https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper67.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">msp.cis.strath.ac.uk/types2025</span><span class="invisible">/abstracts/TYPES2025_paper67.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a></p>
José A. Alonso<p>Readings shared May 30, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/30-readings_shared_05-30-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/05/30-readings_shared_05-30-25</span></a> <a href="https://mathstodon.xyz/tags/AIforCode" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforCode</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/GenerativeAI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>GenerativeAI</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a></p>
José A. Alonso<p>Agent-based logics in dependent type theory. ~ Colm Baston. <a href="https://colmbaston.uk/files/thesis.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">colmbaston.uk/files/thesis.pdf</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a></p>
José A. Alonso<p>Readings shared May 29, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/29-readings_shared_05-29-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/05/29-readings_shared_05-29-25</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Emacs</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Lisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lisp</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch, Axel Ljungström. <a href="https://arxiv.org/abs/2409.02603" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2409.02603</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a></p>
José A. Alonso<p>Mechanized safety of Jolteon consensus in Agda. ~ Orestis Melkonian, Mauro Jaskelioff, and James Chapman. <a href="https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper79.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">msp.cis.strath.ac.uk/types2025</span><span class="invisible">/abstracts/TYPES2025_paper79.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a></p>
Jesper Agdakx 🔸The University of Gothenburg is looking to hire a postdoc for work on<br>compilation of cubical type theory:<br><br> <a href="https://web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=37550" rel="nofollow noopener" target="_blank">web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=37550</a><br><br>Application deadline: June 12.<br><br><a class="hashtag" href="https://agda.club/tag/typetheory" rel="nofollow noopener" target="_blank">#TypeTheory</a> <a class="hashtag" href="https://agda.club/tag/cubical" rel="nofollow noopener" target="_blank">#Cubical</a> <a class="hashtag" href="https://agda.club/tag/hott" rel="nofollow noopener" target="_blank">#HoTT</a> <a class="hashtag" href="https://agda.club/tag/agda" rel="nofollow noopener" target="_blank">#Agda</a> <a class="hashtag" href="https://agda.club/tag/postdoc" rel="nofollow noopener" target="_blank">#PostDoc</a> <a class="hashtag" href="https://agda.club/tag/gothenburg" rel="nofollow noopener" target="_blank">#Gothenburg</a>
José A. Alonso<p>Readings shared May 20, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/20-readings_shared_05-20-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/05/20-readings_shared_05-20-25</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Emacs</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HoTT</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/OrgMode" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>OrgMode</span></a> <a href="https://mathstodon.xyz/tags/Python" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Python</span></a> <a href="https://mathstodon.xyz/tags/Rust" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rust</span></a> <a href="https://mathstodon.xyz/tags/SAT_solvers" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SAT_solvers</span></a> <a href="https://mathstodon.xyz/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TypeTheory</span></a></p>
José A. Alonso<p>Ordinal exponentiation in homotopy type theory. ~ Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. <a href="https://arxiv.org/abs/2501.14542" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2501.14542</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HoTT</span></a></p>
Jesper Agdakx 🔸Here's a first release candidate for <a class="hashtag" href="https://agda.club/tag/agda" rel="nofollow noopener" target="_blank">#Agda</a> 2.8.0! Including (experimental) polarity annotations, error identifiers, a flag for checking a whole library, builtin files included in the Agda binary, and lots of bugfixes.<br><br><a href="https://hackage.haskell.org/package/Agda-2.7.20250510/candidate/changelog" rel="nofollow noopener" target="_blank">hackage.haskell.org/package/Agda-2.7.20250510/candidate/changelog</a>
Christian Tietze<p><span class="h-card" translate="no"><a href="https://tech.lgbt/@cbarrett" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>cbarrett</span></a></span> I guess every place <a href="https://mastodon.social/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> people hang out is a place where noobs hang out because nobody knows anything :D</p>
TrendingLive feeds
Mastodon is the best way to keep up with what's happening.
Follow anyone across the fediverse and see it all in chronological order. No algorithms, ads, or clickbait in sight.
Create accountLoginDrag & drop to upload