teikalang / teika

MIT License
326 stars 7 forks source link

teika: use context during printing #179

Closed EduardoRFS closed 1 year ago

EduardoRFS commented 1 year ago

Goals

Improve error and terms printing.

Context

Due to Teika version of locally nameless names are not available at all in the typed tree, and currently even the ones that are(in binders) are ignored. This patch improves on both dimensions, by having a context for printing where names can be accumulated and by also reading the data available in the typed tree.