Hey all! First-time Coq user here, and I'm having a lot of trouble getting set up. Would someone be willing to help me troubleshoot?
There's a nice tutorial online here, which I'd like to work through: https://cel.archives-ouvertes.fr/inria-00001173v6/document I've downloaded the CoqIDE (for MacOS), but I can't figure out how to run even a simple command like
Check True. in the IDE. I can type the command into the left-hand pane of the IDE, but I have no idea how to actually run it, and I haven't been able to figure it out after clicking through every menu of the interface. According to the tutorial, the correct output would be
True : Prop.
Can someone give me a pointer on how to get started? Apologies for the noobie question, but I'm finding the interface really opaque and couldn't find any tutorials online about how to use the IDE itself.
does the down arrow button not work?
the down arrow immediately right of the x button
Ahhh. Yes, that worked, thank you @Gaëtan Gilbert :face_palm: It appeared to be greyed out and unclickable, but that was a wrong assumption apparently
You should also be able to do cmd + down arrow to step down in the proof if I am not mistaken
Last updated: Jan 31 2023 at 13:02 UTC