4 ms·

Gamifying mathematics (an interactive tutorial for sequent calculus)

• haliax 14y ago
  The linked book by Pierce is pretty fantastic as well. http://www.cis.upenn.edu/~bcpierce/sf/ http://www.cis.upenn.edu/~bcpierce/sf/
• rprospero 14y ago
  I've been working on a similar project for high school algebra. Mine isn't as far along, so it's been nice to see some validation on my ideas, as well as get some thoughts on how I would improve.
• fusiongyro 14y ago
  How do you make contraction happen? I don't see a button for it.
  • ezyang 14y ago
    We do contraction on implication-left automatically, and only have it as an option for forall-left and exists-right, since it's not a useful notion for the other operators.