Fix #7181: Allow matching to continue when stuck on lazy pattern

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.

https://wiki.portal.chalmers.se/agda/pmwiki.php

Other

2.41k stars 339 forks source link

Fix #7181: Allow matching to continue when stuck on lazy pattern #7211

Closed szumixie closed 2 months ago

szumixie commented 2 months ago

Fixes #7181 by allowing reduction to continue matching on the next clause when left-to-right matching is stuck on a lazy pattern while all non-lazy matches fail or succeed.