Skip to content

Instantly share code, notes, and snippets.

@Lysxia Lysxia/A.v
Created Sep 4, 2019

Embed
What would you like to do?
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
You can’t perform that action at this time.