Franklin Pezzuti Dyer (Apr 05 2022 at 17:05): Franklin Pezzuti Dyer (Apr 05 2022 at 17:05):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.
Screen-Shot-2022-04-05-at-11.04.40-AM.png
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.
Gaëtan Gilbert (Apr 05 2022 at 17:13):does the down arrow button not work?
Gaëtan Gilbert (Apr 05 2022 at 17:14):the down arrow immediately right of the x button
Franklin Pezzuti Dyer (Apr 05 2022 at 17:15):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
Ali Caglayan (Apr 05 2022 at 17:15):You should also be able to do cmd + down arrow to step down in the proof if I am not mistaken
Last updated: Sep 23 2023 at 14:01 UTC