Lucas Escot
Lucas Escot
I've come into another regression between current master and the latest release. I'm struggling to find a minimal example, so here is a short file: ```agda {-# OPTIONS --safe --without-K...
There seem to be a regression in the current master of Agda. The following code (where we define the equality type at Setω) ```agda {-# OPTIONS --without-K #-} open import...
Hi all, I just discovered `alot` and so far it has been really good. I was reading about custom pre-command hooks and adding the ["confirm send without attachment"](https://github.com/pazz/alot/issues/395#issuecomment-13859844) hook to...
As disccused in #38 , this PR adds support for the Vim8 Terminal feature. This allows the user to discard tmux entirely and have everything handled inside Vim. Before merging...
I really would like an option similar to [pandoc's `--section-divs` option](https://pandoc.org/MANUAL.html#option--section-divs), so that document sections are properly enclosed, and current selected sections could be properly highlighted. For example, ```md #...
Right now our encoding of telescopes is *overly dependent*. That is, any value in the telescope can appear in any of the types of the rest of the telescope. In...
What we claim in our paper is that it's fine to encode universe-polymorphic datatypes using our descriptions, as long as quantification over levels happen outside of the description. However, currently...
Joint work from @JorisCeulemans, Malin Altenmüller, @anuyts, @flupe and @jpoiret, started during the last AIMXXXI. (This draft co-authored by @jpoiret). This PR introduces *explicit polarity annotations*, as requested in #570...
One interesting feature of ReST is that you can define document variables and meta data directly inside the document, without having to rely on some additional YAML header. For example,...
Bug reported by @liesnikov. ```agda private variable @0 a : Set Ap : (p : @0 a → Set) → @0 a → Set Ap p x = p x...