polarity-lang / polarity

A Language with Dependent Data and Codata Types
https://polarity-lang.github.io
Apache License 2.0
50 stars 0 forks source link

Distinguish two kinds of holes #236

Closed timsueberkrueb closed 2 weeks ago

timsueberkrueb commented 4 months ago

There are two kinds of holes in the surface syntax: ? and _. ? stands for parts of the program that have not been completed yet, and where we expect the compiler to help us with finding the right term to fill in. _ are parts of the program where we expect the compiler to find a unique solution by unification, and where we can't be bothered to write out the term. The compiler should throw an error if it can't find a unique solution for _.