search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
903 stars 58 forks source link

[ test ] add test for defaulting peculiarity #376

Closed gallais closed 4 years ago

gallais commented 4 years ago

In Idris1 one of the expressions leads to a type error even though they are essentially the same. In Idris2 this does not happen. Adding a test case to make sure we do not inadvertently bring this kind of behaviour back.