How De Bruijn Indices are implemented in TinyIdris
Recently, I've been watching the SPLV20 lectures by Edwin Brady and trying to learn more about the implementation of dependent type theories, which is what led to me creating this video.
Recently, I've been watching the SPLV20 lectures by Edwin Brady and trying to learn more about the implementation of dependent type theories, which is what led to me creating this video.