Created
January 31, 2025 09:58
-
-
Save illusory0x0/81d43c7e1466268ee08e477713e8b331 to your computer and use it in GitHub Desktop.
VSCoq word based completion list
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* | |
| word based completion list | |
| https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html | |
| assumption reflexivity trivial auto discriminate exact contradiction Transforming goals | |
| intros / intro simpl unfold apply rewrite inversion left / right replace Breaking apart goals and hypotheses | |
| split destruct (and/or) destruct (case analysis) induction Solving specific types of goals | |
| ring tauto field Tacticals (tactics that act on other tactics) | |
| ; (semicolon) try || (or) all repeat | |
| Require Import | |
| *) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment