From 6ab5cf214cb0af2f6c176f75453c144ab3fe596f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 Jul 2015 18:01:13 -0400 Subject: [PATCH] feat(library,hott): add simp tactic reference --- hott/init/tactic.hlean | 12 ++++++++++++ library/init/tactic.lean | 12 ++++++++++++ 2 files changed, 24 insertions(+) diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 99e29d384d..6cf2a58d0b 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -91,6 +91,18 @@ 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: +-- - d : bool.tt if top-down rewrite strategy +-- - a : bool.tt if assumptions should be used +-- - 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 (d a : bool) (e : expr_list) (n : identifier_list) (x : identifier_list) (t : option tactic) (l : expr) : tactic := builtin + definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin definition induction (h : expr) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin diff --git a/library/init/tactic.lean b/library/init/tactic.lean index eff940036e..389a7fffa5 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -91,6 +91,18 @@ 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: +-- - d : bool.tt if top-down rewrite strategy +-- - a : bool.tt if assumptions should be used +-- - 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 (d a : bool) (e : expr_list) (n : identifier_list) (x : identifier_list) (t : option tactic) (l : expr) : tactic := builtin + definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin definition induction (h : expr) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin