Racket/Dracula

[davidgrenier]

I was wondering if there's a way to use DrRacket + Dracula integration to use J-Bob as an interactive assistant. There's seems to be a panel to the right that indicates it could show me the state of the proof à-là Coq.

My typical mistakes are in the number of arguments or substituting a 't for a '? or that some variable isn't in scope (something a basic type-checker would point out ;-) ) which takes a while to find and all I have to troubleshoot is whether the theorem was accepted or not.