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 😅
1
The assumption in the theorem statement is Thing : Type 0, not _:_ Thing (Type 0)
2
With that fix, I got the proof done.
1
(BTW, I plan to add mix-fix syntax declarations -- in fact, they're basically already implemented.)
1
1
Another confusing thing I plan to fix is that when a rule that introduces new variables is used multiple times it will use the same name each time. I will make Holbert try to disambiguate them a bit.
1
Ahh yeah - I try to rename them when it makes sense to do so, but it would be helpful to do something like that automatically.
1
Oh, also, your pair/introduction rule seems to want Sigma not Pi.
1