rvs314

`chaperone-generics` and `impersonate-vector` don't play well with stream methods

1

**What version of Racket are you using?** 8.15 [cs] **What program did you run?** ```racket #lang racket (module foo racket (provide (contract-out #:forall E (seq->strm (-> (sequence/c E) (stream/c E)))))...

I imagine the `Data.List.Literals` module was intended to allow writing list of characters as string literals (e.g. `"foobar"` becomes `'f' ∷ 'o' ∷ 'o' ∷ 'b' ∷ 'a' ∷ 'r'...

Synthesis fails when `Agda.Builtin.FromString` is in scope

1

Apparently, an internal error occurs when attempting to run mimer if `FromString` is in scope and unqualified definitions are allowed. For example, the error occurs in the following program: ```agda...

Integrate ERI with Emacs' existing formatting infrastructure

1

Is there any plan on integrating ERI with Emacs' existing formatting infrastructure? Currently, agda2-mode just [rebinds `TAB`/`S-TAB`](https://github.com/agda/agda/blob/a9ed8817bec395a270ea56982a91afa9f2ab3c07/src/data/emacs-mode/agda2-mode.el#L260), which is explicitly warned against in the documentation of `indent-line-function`: > Setting this...