agda icon indicating copy to clipboard operation
agda copied to clipboard

Comment on `catchIlltypedPatternBlockedOnMeta` needs update

Open andreasabel opened this issue 2 years ago • 0 comments

@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.

andreasabel avatar Jan 02 '24 06:01 andreasabel