Mark Barbone

Idris 2 implementation

1

In this implementation, I took the liberty of not following the guide to the letter. For example, there's no special-forms switch statement, or TCO loop, or functions with underscores. Instead,...

Internal error

1

I'm trying to go through the NbE example, and got an internal error. I've simplified it to this: ``` $ cat bug.bel LF tm : type = | abs :...

Bad matches for grammars that require backtracking

5

This lexical grammar is ambiguous with only one character lookahead and no backtracking: ```rust #[derive(Logos, Debug)] enum Token { #[error] Error, #[token("a")] A, #[token("axb")] B, #[regex("ax[bc]")] Word, } ``` It...

Currently, if I type (in insert mode) `"some text`, delimitMate helpfully makes it `"some text"`. However, if I type `"text \" with an escaped quote`, delimitMate sees the quote, doesn't...

Make `foldl/4` error outside its domain

1

Use single-sided unification rules for `foldl/4` so that something like `foldl(not_a_list, Goal, In, Out)` is an exception instead of silently failing. This would be a breaking change. Some unresolved questions:...

While I don't have an older version of Agda to test with, the docs only mentioned 2.5.* that I saw, so I assume this is a compatibility issue with a...

It talked about `t1` and `t2` within a term `{x : T = t} - t2`. I believe that term should read `{x : T = t1} - t2`. I...

'a' should be callable

2

Scryer Prolog assures me that `'a'` and `a` are the same thing, but `'a'.` and `a.` give different errors in the REPL: ``` $ scryer-prolog ?- 'a' = a. true....

With the new update, the "Prime Factor" screen is unable to show the factorization of integers when they are too large. It's not a problem with the `FactorInteger` routine, which...

Possible issue with shrinkTerm?

1

I'm not certain if this is expected/desired behavior or not. Currently, when `shrinkTerm` encounters a metavariable, it fails if any argument is not in the smaller context: https://github.com/idris-lang/Idris2/blob/891b2d667ab9ef2f12aaaf372494ad680a494be5/src/Core/TT.idr#L1086-L1093 This is...