I have nearly the same comments as for UniMath/largecatmodules#160. The difference is that in TypeTheory, the option -type-in-type has already been removed.
Analogous to the suggested solution for that issue, the file name below has been suffixed with .txt so as to be acceptable as an attachment to this issue. Interestingly, -R does not seem to be needed - -Q suffices.
.dir-locals.el.txt
I have nearly the same comments as for UniMath/largecatmodules#160. The difference is that in TypeTheory, the option
-type-in-typehas already been removed.Analogous to the suggested solution for that issue, the file name below has been suffixed with .txt so as to be acceptable as an attachment to this issue. Interestingly,
-Rdoes not seem to be needed --Qsuffices..dir-locals.el.txt