bidirectional type checking but now its cardinal directions (north, south, east, west)
@koronkebitchpaulette d. koronkevich Top Level Expression
You are standing at the top of a lambda term with no annotation on the binder. Possible exits are NORTH, SOUTH, and EAST.
⊢ go east
You find yourself at the border of a dense forest of infix operators, the precedence of which depends upon elaboration. Many who have entered are fabled to have diverged and never returned. Possible exits are WEST and SOUTH.
⊢ go south
You enter the forest. A witch turns you into a stuck term.
GAME OVER. Backtrack and try again?
If you have a fediverse account, you can quote this note from your own instance. Search https://mastodon.social/users/lexi_lambda/statuses/116055664328795087 on your instance and quote it. (Note that quoting is not supported in Mastodon.)