Skip to content

Instantly share code, notes, and snippets.

@andres-erbsen
Created December 6, 2018 04:17
Show Gist options
  • Save andres-erbsen/889c559cc7b4096a7e284eae3989bf1f to your computer and use it in GitHub Desktop.
Save andres-erbsen/889c559cc7b4096a7e284eae3989bf1f to your computer and use it in GitHub Desktop.
Ltac fork :=
multimatch constr:(Set) with
| _ => true
| _ => false
end.
Goal True.
let x := fork in
idtac x;
unify x false.
(* true *)
(* false *)
Abort.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment