michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(hott/init/tactic): add replace

Browse source
This commit is contained in:
Floris van Doorn 2016-02-04 22:30:39 -05:00 committed by Leonardo de Moura
parent 668758c44e
commit ec38ee8df8
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
hott/init/tactic.hlean
View file

@ -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)