Fix #7236: use context rather than telescope for lambda-bound variables in rewrite patterns

agda / agda

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

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

Other

2.4k stars 339 forks source link

Fix #7236: use context rather than telescope for lambda-bound variables in rewrite patterns #7237

Closed andreasabel closed 1 month ago

andreasabel commented 1 month ago

Debug #7236: print NLPat with hiding (was previously simply dropped)
WIP: Fix #7236: context instead of telescope for lambda-bound pattern vars

Closes #7236.

andreasabel commented 1 month ago

@jespercockx : ~~This is for now a proof of concept; e.g. I have not implemented the MonadFresh for NLP properly. (The Names in Context are a bit annoying for this purpose of contexts here.)~~ (Update: I discovered that ReduceM already supports MonadFresh.) Let me know what you think of this solution.