idris-lang / Idris2

A purely functional programming language with first class types

https://idris-lang.org/

Other

2.53k stars 380 forks source link

[ test ] Add issue#1988 to the test suite #3238

Closed CodingCellist closed 8 months ago

CodingCellist commented 8 months ago

Description

Issue #1988 appears to be fixed now, presumably thanks to PR #3108 or similar. This came up when I was looking through the proof of false tagged things, thanks to a question in the Discord. Thought it best to add the issue case to the test suite, just for good measure : )

Closes #1988

Should this change go in the CHANGELOG?

Don't think so

andrevidela commented 8 months ago

Let's gooooo

dunhamsteve commented 8 months ago

It was brought up on discord that the case at the top of issue #1988 (the version with the lam) is still accepted by Idris. The reduced test case, included here, is properly rejected by Idris.