From c2602baf2b34911fec195d66ebab5106ea5bf441 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Nov 2014 19:33:11 -0800 Subject: [PATCH] feat(library/tools/tactic): add 'cases' alias for 'inversion' tactic --- library/tools/tactic.lean | 1 + src/emacs/lean-syntax.el | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean index cbad48940..1ec2c52ea 100644 --- a/library/tools/tactic.lean +++ b/library/tools/tactic.lean @@ -58,6 +58,7 @@ opaque definition unfold (e : expr) : tactic := builtin opaque definition exact (e : expr) : tactic := builtin opaque definition trace (s : string) : tactic := builtin opaque definition inversion (e : expr) : tactic := builtin +definition cases := inversion notation a `↦` b := rename a b diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 89cd2bdd0..87e5a1bb7 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -123,7 +123,7 @@ (,(rx (not (any "\.")) word-start (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "rename" "intro" "intros" "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat" - "whnf" "rotate" "rotate_left" "rotate_right" "inversion") + "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases") word-end) . 'font-lock-constant-face) ;; Types