I've just added a minor new feature to Holbert. You can now load a file from a URL automatically by specifying it as the URL query string. E.g. 's gist on MLTT in Holbert can be loaded automatically and shared with a single link:
liamoc.net/holbert/?https
Conversation
Oooh neat. I wonder if there is a way to get the latest version somehow… not sure if Gist's have a special URL for that… 🤔
1
1
You can now see how I got stuck on a proof at the bottom 😅
Replying to
The assumption in the theorem statement is Thing : Type 0, not _:_ Thing (Type 0)
2
With that fix, I got the proof done.
1
Show replies