search

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

No reproducer for error raised in `telePiPath` #7226

Open andreasabel opened 2 months ago

andreasabel commented 2 months ago

The testsuite does not cover this error atm: https://github.com/agda/agda/blob/8c52e3f71c890314c1436a55193256d2b1a43f35/src/full/Agda/TypeChecking/Telescope/Path.hs#L44-L52