I found this about implementing Imp[0] in Coq (which is the language he writing tree-sitter for) to be interesting as well. [0]: https://softwarefoundations.ci

I found this about implementing Imp[0] in Coq (which is the language he writing tree-sitter for) to be interesting as well. [0]: https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html https://softwarefoundations.cis.upenn.edu/lf-current/Imp.htm...