Skip to content

Instantly share code, notes, and snippets.

@Lysxia

Lysxia/A.v

Created September 4, 2019 15:13
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Lysxia/d286cf0197a3bf40608c8dd101ff4fc4 to your computer and use it in GitHub Desktop.
Save Lysxia/d286cf0197a3bf40608c8dd101ff4fc4 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
A.v
Goal (0 = 0 /\ 1 = 1).
Proof.
split.
all: reflexivity.
Qed.
Ltac foo := split.
Goal (0 = 0 /\ 1 = 1).
Proof.
foo.
all: reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment