Hi. Thanks for making this great project I have really enjoyed playing with agda through it. I was trying to play the HoTT game https://homotopytypetheory.org/2021/12/01/the-hott-game/ lately and got stuck on quest 0. The reason is that I cannot enter control-n nor control-t in my chrome browser in agdapad. The browser eats the keystroke as a command and opens a new window or tab. I wonder if it would be possible to create some sort of key remapping or other feature so that control-n and control-t can be entered into agdapad? That way I could do the normalization and finish quest 0 in the HoTT game.
Hi. Thanks for making this great project I have really enjoyed playing with agda through it. I was trying to play the HoTT game https://homotopytypetheory.org/2021/12/01/the-hott-game/ lately and got stuck on quest 0. The reason is that I cannot enter control-n nor control-t in my chrome browser in agdapad. The browser eats the keystroke as a command and opens a new window or tab. I wonder if it would be possible to create some sort of key remapping or other feature so that control-n and control-t can be entered into agdapad? That way I could do the normalization and finish quest 0 in the HoTT game.