Closed jonweinb closed 1 year ago
I noticed the extension .rzk
is omitted for other files referenced in that document as well. Perhaps this is intentional?
Maybe just a leftover, feel free to go ahead and fix @fredrik-bakke (whenever you get around to it)
Thanks all. I think this is ready to merge. I just added the new file to the web table of contents (by updating the mkdocs file).
See https://github.com/rzk-lang/sHoTT/issues/87