diff options
Diffstat (limited to 'src/Util/Tactics')
| -rw-r--r-- | src/Util/Tactics/TransparentAssert.v | 8 |
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. |