Dungeon Proof Crawler: learn how to write proofs with RPG
dhilst.github.io
Dungeon Proof Crawler: learn how to write proofs with RPG
1–10 of 28 posts
Re: Dungeon Proof Crawler: learn how to write proofs with RPG
#2Surprisingly interesting experience even for someone that does know nothing about writing proof - thanks to gradual onboarding and a decent help menu.
Also, perfectly playable at mobile (at least a couple of first monsters).
Re: Dungeon Proof Crawler: learn how to write proofs with RPG
#3The first and southwest-most sphinxes of seed 0 never load, which soft-locks the game. (Fortunately it doesn't corrupt the save-file.)
Edit: after fighting enough other sphinxes, the first one loads, but the west-most fails with an explicit error message:
> This challenge failed to load. Retreating.
On the next floor, the sphinx over the exit stairs fails, preventing me from progressing.
Re: Dungeon Proof Crawler: learn how to write proofs with RPG
#4Surprisingly interesting experience even for someone that does know nothing about writing proof - thanks to gradual onboarding and a decent help menu. Also, perfectly playable at mobile (at least a couple of first monsters).
I had the exact opposite experience. It doesn't teach the basics needed to even solve the first puzzle. Which language are we even writing in? Clicking help explains what exactly to do but not why, as well as lots of rules with unexplained terminology.
Re: Dungeon Proof Crawler: learn how to write proofs with RPG
#5Surprisingly interesting experience even for someone that does know nothing about writing proof - thanks to gradual onboarding and a decent help menu. Also, perfectly playable at mobile (at least a couple of first monsters).
I had the exact opposite experience. It doesn't teach the basics needed to even solve the first puzzle. Which language are we even writing in? Clicking help explains what exactly to do but not why, as well as lots of rules with unexplained terminology.
There's a chance it's this: https://github.com/dhilst/algae
Re: Dungeon Proof Crawler: learn how to write proofs with RPG
#6I thought this was about writing proofs with RPG the programming language and I was intrigued.
To make it clear that it is with an RPG (role playing game) it needs an "an" in the title.
Re: Dungeon Proof Crawler: learn how to write proofs with RPG
#7I thought this was about writing proofs with RPG the programming language and I was intrigued. To make it clear that it is with an RPG (role playing game) it needs an "an" in the title.
"Every monster is a proof. Bring back the ring before sunrise."
Re: Dungeon Proof Crawler: learn how to write proofs with RPG
#8I sort of reverse engineered the first couple riddles (the help menu helped too) before really getting the logic here.
What I gathered:
- the paramaeters in lemma banish() are "given" - the statement right after lemma banish() is what we want to prove - all "wip" needs to replaced by something - blocks need to be finished with "qed;"
From there it's using the available tools.
Re: Dungeon Proof Crawler: learn how to write proofs with RPG
#9Such a great idea!
Re: Dungeon Proof Crawler: learn how to write proofs with RPG
#10Earlier quoted context omitted.
I had the exact opposite experience. It doesn't teach the basics needed to even solve the first puzzle. Which language are we even writing in? Clicking help explains what exactly to do but not why, as well as lots of rules with unexplained terminology.
There's a chance it's this: https://github.com/dhilst/algae
Interactive thingy here, and a tutorial: