max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/meta/congr_tactic): export congr as an interactive tactic

Browse source
This commit is contained in:
Gabriel Ebner 2017-08-29 16:34:59 +02:00
parent 05178ad950
commit eda1efcb5f
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/init/meta/congr_tactic.lean
View file

@ -56,4 +56,11 @@ do focus1 (try assumption >> congr_core >> all_goals (try reflexivity >> try con
meta def rel_congr : tactic unit :=
do focus1 (try assumption >> rel_congr_core >> all_goals (try reflexivity))
namespace interactive
meta def congr := tactic.congr
meta def rel_congr := tactic.rel_congr
end interactive
end tactic