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

chore(hott/library): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-17 11:31:07 -08:00
parent 2502039a5c
commit 13419d1561
2 changed files with 0 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
hott/init/tactic.hlean
View file

@ -91,15 +91,6 @@ definition rewrite_tac (e : expr_list) : tactic := builtin
definition xrewrite_tac (e : expr_list) : tactic := builtin
definition krewrite_tac (e : expr_list) : tactic := builtin
-- simp_tac is just a marker for the builtin 'simp' notation
-- used to create instances of this tactic.
-- Arguments:
-- - e : additional rewrites to be considered
-- - n : add rewrites from the give namespaces
-- - x : exclude the give global rewrites
-- - t : tactic for discharging conditions
-- - l : location
definition simp_tac (e : expr_list) (n : identifier_list) (x : identifier_list) (t : option tactic) (l : expr) : tactic := builtin
-- Arguments:
-- - ls : lemmas to be used (if not provided, then blast will choose them)
-- - ds : definitions that can be unfolded (if not provided, then blast will choose them)

9
library/init/tactic.lean
View file

@ -92,15 +92,6 @@ definition rewrite_tac (e : expr_list) : tactic := builtin
definition xrewrite_tac (e : expr_list) : tactic := builtin
definition krewrite_tac (e : expr_list) : tactic := builtin
-- simp_tac is just a marker for the builtin 'simp' notation
-- used to create instances of this tactic.
-- Arguments:
-- - e : additional rewrites to be considered
-- - n : add rewrites from the give namespaces
-- - x : exclude the give global rewrites
-- - t : tactic for discharging conditions
-- - l : location
definition simp_tac (e : expr_list) (n : identifier_list) (x : identifier_list) (t : option tactic) (l : expr) : tactic := builtin
-- Arguments:
-- - ls : lemmas to be used (if not provided, then blast will choose them)
-- - ds : definitions that can be unfolded (if not provided, then blast will choose them)