Jonathan Chan

It was looping over a hashtable so there isn't a comprehensible order idk if `#:sort-by` is a good key name or if there's a different convention

[Issue #709] Based on [Agda's lexer](https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Parser/Lexer.x), I've filled out the remaining bits of the Agda lexer. It doesn't quite match the behaviour, especially in places where the semantics of the...

Can't apply erased arguments to kinds imported from parametrized module

1

Suppose I had a file with the following: ``` module P (T: ★) {t: T}. U : ★ = T. 𝒌 = ★. ``` In a different file where I...

Compilation error at Builtin.idr with Chez Scheme

5

Chez Scheme version: 9.5.8, installed from AUR Idris version: 38caff23b8b9f1fc9a7a55d73fa10fe4e7cf7b79 Running the following: ```bash make clean make bootstrap-clean make distclean make bootstrap SCHEME=chez ``` After a while, I reach this...

Unexpected token `mutual` after docstring comment

1

### Prerequisites Please put an X between the brackets as you perform the following steps: * [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [X] Reduce the...