From baed98d5bebcb297bca1e64c840721127d21e618 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2014 10:14:57 -0800 Subject: [PATCH] chore(builtin/kernel): adjust emacs mode and fix typo Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 2 +- src/emacs/lean-mode.el | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index eadd7f338..53607ac7f 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -201,7 +201,7 @@ theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b (λ Hbt : b = true, false_elim (a = b) (subst (Hba (eqt_elim Hbt)) Haf)) (λ Hbf : b = false, trans Haf (symm Hbf))) -theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b +theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a ↔ b := boolext Hab Hba theorem eqt_intro {a : Bool} (H : a) : a = true diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 48637ac5f..81c51c872 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -28,7 +28,7 @@ '(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face) ("\\_<\\(calc\\|have\\|in\\|let\\|forall\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face) ("\"[^\"]*\"" . 'font-lock-string-face) - ("\\(->\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-⟷]\\)" . 'font-lock-constant-face) + ("\\(->\\|↔\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-]\\)" . 'font-lock-constant-face) ("\\(λ\\|→\\|∃\\|∀\\|:\\|:=\\)" . font-lock-constant-face) ("\\_<\\(\\b.*_tac\\|Cond\\|OrElse\\|T\\(?:hen\\|ry\\)\\|When\\|apply\\|b\\(?:ack\\|eta\\)\\|done\\|exact\\)\\_>" . 'font-lock-constant-face) ("\\(universe\\|theorem\\|axiom\\|definition\\|variable\\|builtin\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-function-name-face))