Michael Arntzenius
Michael Arntzenius
On Ubuntu 22.04 LTS and perhaps other Linux distros, Firefox and Chrome get installed as Snap packages, which are isolated in some way I don't fully understand from the local...
When using racket-mode and paredit-mode together, `paredit-open-round` reindents more aggressively than it should (or at least, more aggressively than it does in other modes, such as scheme-mode and lisp-mode). For...
Agda has pattern synonyms; why not copattern synonyms? Some (admittedly not very motivating) possible examples: ```agda copattern π₁ t = proj₁ t copattern π₂ t = proj₁ (proj₂ t) copattern...
confusing error message for unannotated definition in `where` block attached to polymorphic function
```idris two: Nat two = 2 bar: a -> a bar x = x where wat = two ``` yields the error message: ``` While processing right hand side of...
```idris bar = 3 where wat = 2 baz = 3 where wat = 2 ``` Produces the error: ``` While processing right hand side of baz. Main.wat is already...
With Idris 2, version 0.5.1-68a144bf1. The following code: ``` interface Cat obj (hom: obj -> obj -> Type) where id : hom a a ``` produces the error: ``` While...
The tutorial page on "Interactive Editing" (https://idris2.readthedocs.io/en/latest/tutorial/interactive.html) claims the idris2 repl supports a command `:addmissing` (synonym `:am`). As far as I can tell it does not. It is not listed...
I'm using agda version 2.5.4.1-6b1d87f. Say I have the following: ```agda data ⊤ : Set where tt : ⊤ foo : {{x : ⊤}} -> ⊤ foo {{x}} = {!x!}...
**How to replicate:** Make a directory with two files, `A.hs` and `B.hs`, like so: ``` -- In A.hs: module A where {} -- In B.hs: import A x = unbound...
emacs 28.2 eglot-jl 2.2.1 eglot 1.15 I have a large julia project which is also a git repository and contains large (~1GB) downloaded text data files. These are gitignored. Before...