Add TransparentAssert

1 files changed, 8 insertions, 0 deletions

diff --git a/src/Util/Tactics/TransparentAssert.v b/src/Util/Tactics/TransparentAssert.v
new file mode 100644
index 000000000..533d159f7
--- /dev/null
+++ b/src/Util/Tactics/TransparentAssert.v
@@ -0,0 +1,8 @@
+(** [transparent assert (H : T)] is like [assert (H : T)], but leaves the body transparent. *)
+Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" :=
+  simple refine (let name := (_ : type) in _).
+
+(** [transparent eassert] is like [transparent assert], but allows holes in the type, which will be turned into evars. *)
+Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" "by" tactic3(tac) := let name := fresh "H" in transparent assert (name : type); [ solve [ tac ] | ].
+Tactic Notation "transparent" "eassert" "(" ident(name) ":" open_constr(type) ")" := transparent assert (name : type).
+Tactic Notation "transparent" "eassert" "(" ident(name) ":" open_constr(type) ")" "by" tactic3(tac) := transparent assert (name : type) by tac.