agda
agda copied to clipboard
Comment on `catchIlltypedPatternBlockedOnMeta` needs update
@UlfNorell, please have a look at this comment and update it to the current situation: https://github.com/agda/agda/blob/5d25cf8ef920310341a782b11bb51ad7462a2902/src/full/Agda/TypeChecking/Rules/Term.hs#L824-L827
- There is no more meta returned or passed to the continuation. Instead, there is a
Blocker. - Does the comment still apply to the blocker?
Raised in https://github.com/agda/agda/commit/552987aa0119f2bca5eaf4dca7934e37209112f9#r136034513.