blob: 576aab0e0f5b6c68d104c6f3c5c3f2d3bf0c75a1 (
plain)
1
2
3
4
5
6
7
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) := 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.
|
