stagedtt icon indicating copy to clipboard operation
stagedtt copied to clipboard
verified publisher icon RedPRL

🕳️ ⛳ Type Holes

Open TOTBWF opened this issue 3 years ago • 0 comments

Patch Description

This PR adds type holes, as well as some error reporting infrastructure. Such is life when we start a new proof assistant, hard to work on one thing at once!

Checklist

  • [ ] Have the elaborator track/return if a term has a hole.
  • [ ] Track what terms contain holes in the globals.

TOTBWF avatar May 13 '22 01:05 TOTBWF