diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-05 10:29:59 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-04-05 10:29:59 -0400 |
commit | 2a94c03e5326020d63dd5a1afd4ab514ffb30a81 (patch) | |
tree | 477f513ae3734d6d132d7662d22f24ae87e0a646 /src | |
parent | 8e6549d776ab2e60d4a669d37dd7b2df9becc592 (diff) |
Add TransparentAssert
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/Tactics.v | 1 | ||||
-rw-r--r-- | src/Util/Tactics/TransparentAssert.v | 8 |
2 files changed, 9 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 3c1367fae..a54982a17 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -32,6 +32,7 @@ Require Export Crypto.Util.Tactics.SplitInContext. Require Export Crypto.Util.Tactics.SubstEvars. Require Export Crypto.Util.Tactics.SubstLet. Require Export Crypto.Util.Tactics.Test. +Require Export Crypto.Util.Tactics.TransparentAssert. Require Export Crypto.Util.Tactics.UnifyAbstractReflexivity. Require Export Crypto.Util.Tactics.UniquePose. Require Export Crypto.Util.Tactics.VM. 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. |