From ec38ee8df81ab7b873c8e31b295b05aaec9ed4df Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 4 Feb 2016 22:30:39 -0500 Subject: [PATCH] fix(hott/init/tactic): add replace --- hott/init/tactic.hlean | 1 + 1 file changed, 1 insertion(+) diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index b5ca7b6e36..cd53a8dc7e 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -95,6 +95,7 @@ definition trace (s : string) : tactic := builtin definition rewrite_tac (e : expr_list) : tactic := builtin definition xrewrite_tac (e : expr_list) : tactic := builtin definition krewrite_tac (e : expr_list) : tactic := builtin +definition replace (old : expr) (new : with_expr) (loc : location) : tactic := builtin -- Arguments: -- - ls : lemmas to be used (if not provided, then blast will choose them)