Skip to content

Instantly share code, notes, and snippets.

@mheiber

mheiber/dubstep.v

Created August 1, 2020 22:18
Show Gist options
  • Save mheiber/a0a4cf88e05018f1b25925a4080aae37 to your computer and use it in GitHub Desktop.
Save mheiber/a0a4cf88e05018f1b25925a4080aae37 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
dubstep.v
Ltac dubstep_goal F :=
unfold F; fold F.
Ltac dubstep_in F H :=
unfold F in H; fold F in H.
Tactic Notation "dubstep" constr(F) := (dubstep_goal F).
Tactic Notation "dubstep" constr(F) "in" hyp(H) := (dubstep_in F H).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment