idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-17 08:11:45 +03:00
Code Issues Projects Releases Wiki Activity
663a8381f4
Idris2/tests/idris2/reg040
History
Edwin Brady 663a8381f4 Properly normalise constants on LHS 
We need to fully evaluate, not just the public export names, otherwise
we don't pattern match properly and potentially generate catch all
patterns we don't mean.

Fixes #1537
2021-06-11 12:37:45 +01:00
..
CoverBug.idr Properly normalise constants on LHS 2021-06-11 12:37:45 +01:00
expected Properly normalise constants on LHS 2021-06-11 12:37:45 +01:00
run Properly normalise constants on LHS 2021-06-11 12:37:45 +01:00