From 2a94c03e5326020d63dd5a1afd4ab514ffb30a81 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 5 Apr 2017 10:29:59 -0400 Subject: Add TransparentAssert --- src/Util/Tactics/TransparentAssert.v | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 src/Util/Tactics/TransparentAssert.v (limited to 'src/Util/Tactics') 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. -- cgit v1.2.3