Comment on catchIlltypedPatternBlockedOnMeta
needs update
#7045
Labels
bit-rot
Functionality broken by refactorings etc.
type: task
Concerning the development of Agda (not in changelog)
Milestone
@UlfNorell, please have a look at this comment and update it to the current situation:
agda/src/full/Agda/TypeChecking/Rules/Term.hs
Lines 824 to 827 in 5d25cf8
Blocker
.Raised in 552987a#r136034513.
The text was updated successfully, but these errors were encountered: