feat(library/tactic): make let tactic transparent, introduce new opaque note tactic

The new let tactic is semantically equivalent to let terms, while `note`
preserves its old opaque behavior.

hott/algebra/category/functor/adjoint.hlean

@@ -124,12 +124,12 @@ namespace category
     fapply nat_trans.mk: esimp,
     { intro c, exact natural_map (to_hom θ) (c, F c) id},
     { intro c c' f,
-      let H := naturality (to_hom θ) (ID c, F f),
+      note H := naturality (to_hom θ) (ID c, F f),
-      let K := ap10 H id,
+      note K := ap10 H id,
       rewrite [▸* at K, id_right at K, ▸*, K, respect_id, +id_right],
       clear H K,
-      let H := naturality (to_hom θ) (f, ID (F c')),
+      note H := naturality (to_hom θ) (f, ID (F c')),
-      let K := ap10 H id,
+      note K := ap10 H id,
       rewrite [▸* at K, respect_id at K,+id_left at K, K]}
   end
 
@@ -138,12 +138,12 @@ namespace category
     fapply nat_trans.mk: esimp,
     { intro d, exact natural_map (to_inv θ) (G d, d) id, },
     { intro d d' g,
-      let H := naturality (to_inv θ) (Gᵒᵖᶠ g, ID d'),
+      note H := naturality (to_inv θ) (Gᵒᵖᶠ g, ID d'),
-      let K := ap10 H id,
+      note K := ap10 H id,
       rewrite [▸* at K, id_left at K, ▸*, K, respect_id, +id_left],
       clear H K,
-      let H := naturality (to_inv θ) (ID (G d), g),
+      note H := naturality (to_inv θ) (ID (G d), g),
-      let K := ap10 H id,
+      note K := ap10 H id,
       rewrite [▸* at K, respect_id at K,+id_right at K, K]}
   end
 
@@ -151,8 +151,8 @@ namespace category
     : natural_map (to_hom θ) (c, d) f = G f ∘ adj_unit c :=
   begin
     esimp,
-    let H := naturality (to_hom θ) (ID c, f),
+    note H := naturality (to_hom θ) (ID c, f),
-    let K := ap10 H id,
+    note K := ap10 H id,
     rewrite [▸* at K, id_right at K, K, respect_id, +id_right],
   end
 
@@ -160,8 +160,8 @@ namespace category
     : natural_map (to_inv θ) (c, d) g = adj_counit d ∘ F g :=
   begin
     esimp,
-    let H := naturality (to_inv θ) (g, ID d),
+    note H := naturality (to_inv θ) (g, ID d),
-    let K := ap10 H id,
+    note K := ap10 H id,
     rewrite [▸* at K, id_left at K, K, respect_id, +id_left],
   end
 

hott/cubical/pathover2.hlean

@@ -109,7 +109,7 @@ namespace eq
   begin
     rewrite [apdo_eq_apdo_ap _ _ p],
     let y := !change_path_of_pathover (apdo (apdo id) (ap_constant p b))⁻¹ᵒ,
-    rewrite -y, esimp, clear y,
+    rewrite -y, esimp,
     refine !pathover_ap_pathover_of_pathover_ap ⬝ _,
     rewrite pathover_ap_change_path,
     rewrite -change_path_con, apply ap (λx, change_path x idpo),

hott/cubical/squareover.hlean

@@ -146,7 +146,7 @@ namespace eq
                            (pathover_idp_of_eq l)
                            (pathover_idp_of_eq r)) : square t b l r :=
   begin
-    let H := square_of_squareover so,  -- use apply ... in
+    note H := square_of_squareover so,  -- use apply ... in
     rewrite [▸* at H,+idp_con at H,+ap_id at H,↑pathover_idp_of_eq at H],
     rewrite [+to_right_inv !(pathover_equiv_tr_eq (refl a)) at H],
     exact H
@@ -230,7 +230,7 @@ namespace eq
   definition eq_of_vdeg_squareover {q₁₀' : b₀₀ =[p₁₀] b₂₀}
     (p : squareover B vrfl q₁₀ q₁₀' idpo idpo) : q₁₀ = q₁₀' :=
   begin
-    let H := square_of_squareover p,  -- use apply ... in
+    note H := square_of_squareover p,  -- use apply ... in
     induction p₁₀, -- if needed we can remove this induction and use con_tr_idp in types/eq2
     rewrite [▸* at H,idp_con at H,+ap_id at H],
     let H' := eq_of_vdeg_square H,

hott/homotopy/circle.hlean

@@ -263,7 +263,7 @@ namespace circle
     induction x,
     { apply base_eq_base_equiv},
     { apply equiv_pathover, intro p p' q, apply pathover_of_eq,
-      let H := eq_of_square (square_of_pathover q),
+      note H := eq_of_square (square_of_pathover q),
       rewrite con_comm_base at H,
       let H' := cancel_left H,
       induction H', reflexivity}

hott/homotopy/join.hlean

@@ -128,7 +128,7 @@ namespace join
     (c : cube s₀₁₁ vrfl s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) :
     cube s₁₁₂⁻¹ᵛ vrfl (massage_sq s₁₀₁) (massage_sq s₁₂₁) s₁₁₀⁻¹ᵛ s₀₁₁⁻¹ᵛ :=
   begin
-    cases p₁₀₀, cases p₁₀₂, cases p₁₂₂, let c' := massage_cube' c, esimp[massage_sq],
+    cases p₁₀₀, cases p₁₀₂, cases p₁₂₂, note c' := massage_cube' c, esimp[massage_sq],
     krewrite vdeg_v_eq_ph_pv_hp at c', exact c',
   end
 

hott/homotopy/sphere.hlean

@@ -188,7 +188,7 @@ namespace is_trunc
     (a : A) (f : map₊ (S. n) (pointed.Mk a)) (x : S n) : f x = f base :=
   begin
     let H' := iff.elim_left (is_trunc_iff_is_contr_loop n A) H a,
-    let H'' := @is_trunc_equiv_closed_rev _ _ _ !pmap_sphere H',
+    note H'' := @is_trunc_equiv_closed_rev _ _ _ !pmap_sphere H',
     assert p : (f = pmap.mk (λx, f base) (respect_pt f)),
       apply is_hprop.elim,
     exact ap10 (ap pmap.map p) x

hott/init/tactic.hlean

@@ -126,7 +126,7 @@ definition change (e : expr) : tactic := builtin
 
 definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
 
-definition lettac (id : identifier) (e : expr) : tactic := builtin
+definition notetac (id : identifier) (e : expr) : tactic := builtin
 
 definition constructor (k : option num)  : tactic := builtin
 definition fconstructor (k : option num) : tactic := builtin

hott/types/univ.hlean

@@ -52,10 +52,10 @@ namespace univ
     intro f,
     have u : ¬¬bool, by exact (λg, g tt),
     let H1 := apdo f eq_bnot,
-    let H2 := apo10 H1 u,
+    note H2 := apo10 H1 u,
     have p : eq_bnot ▸ u = u, from !is_hprop.elim,
     rewrite p at H2,
-    let H3 := eq_of_pathover_ua H2, esimp at H3, --TODO: use apply ... at after #700
+    note H3 := eq_of_pathover_ua H2, esimp at H3, --TODO: use apply ... at after #700
     exact absurd H3 (bnot_ne (f bool u)),
   end
 

library/data/int/order.lean

@@ -388,7 +388,7 @@ theorem exists_least_of_bdd {P : ℤ → Prop} [HP : decidable_pred P]
     have Hzbk : z = b + of_nat (nat_abs (z - b)),
       by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add_comm, sub_add_cancel],
     have Hk : nat_abs (z - b) < least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b))), begin
-     let Hz' := iff.mp !lt_add_iff_sub_lt_left Hz,
+     note Hz' := iff.mp !lt_add_iff_sub_lt_left Hz,
      rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'],
      apply lt_of_of_nat_lt_of_nat Hz'
     end,
@@ -426,7 +426,7 @@ theorem exists_greatest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P]
     have Hzbk : z = b - of_nat (nat_abs (b - z)),
       by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), sub_sub_self],
     have Hk : nat_abs (b - z) < least (λ n, P (b - of_nat n)) (nat.succ (nat_abs (b - elt))), begin
-      let Hz' := iff.mp !lt_add_iff_sub_lt_left (iff.mpr !lt_add_iff_sub_lt_right Hz),
+      note Hz' := iff.mp !lt_add_iff_sub_lt_left (iff.mpr !lt_add_iff_sub_lt_right Hz),
       rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'],
       apply lt_of_of_nat_lt_of_nat Hz'
     end,

library/data/real/basic.lean

@@ -36,8 +36,8 @@ private theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq :
   (H : n ≥ pceil (q / ε)) :
         q * n⁻¹ ≤ ε :=
 begin
-  let H2 := pceil_helper H (div_pos_of_pos_of_pos Hq Hε),
+  note H2 := pceil_helper H (div_pos_of_pos_of_pos Hq Hε),
-  let H3 := mul_le_of_le_div (div_pos_of_pos_of_pos Hq Hε) H2,
+  note H3 := mul_le_of_le_div (div_pos_of_pos_of_pos Hq Hε) H2,
   rewrite -(one_mul ε),
   apply mul_le_mul_of_mul_div_le,
   repeat assumption
@@ -138,7 +138,7 @@ private theorem factor_lemma (a b c d e : ℚ) : abs (a + b + c - (d + (b + e)))
 
 private theorem factor_lemma_2 (a b c d : ℚ) : (a + b) + (c + d) = (a + c) + (d + b) :=
 begin
-   let H := (binary.comm4 add.comm add.assoc a b c d),
+   note H := (binary.comm4 add.comm add.assoc a b c d),
    rewrite [add.comm b d at H],
    exact H
 end
@@ -773,7 +773,7 @@ theorem equiv_of_diff_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t)
                          ... = b + d + a + e + c   : add.comm,
     apply eq_of_bdd Hs Ht,
     intros,
-    let He := bdd_of_eq H,
+    note He := bdd_of_eq H,
     existsi 2 * (2 * (2 * j)),
     intros n Hn,
     rewrite (rewrite_helper5 _ _ (s (2 * n)) (t (2 * n))),
@@ -908,7 +908,7 @@ theorem zero_nequiv_one : ¬ zero ≡ one :=
   begin
     intro Hz,
     rewrite [↑equiv at Hz, ↑zero at Hz, ↑one at Hz],
-    let H := Hz (2 * 2),
+    note H := Hz (2 * 2),
     rewrite [zero_sub at H, abs_neg at H, pnat.add_halves at H],
     have H' : pone⁻¹ ≤ 2⁻¹, from calc
       pone⁻¹ = 1 : by rewrite -pone_inv

library/data/real/complete.lean

@@ -472,7 +472,7 @@ theorem le_ceil (x : ℝ) : x ≤ ceil x :=
 theorem lt_of_lt_ceil {x : ℝ} {z : ℤ} (Hz : z < ceil x) : z < x :=
   begin
     rewrite ↑ceil at Hz,
-    let Hz' := lt_of_floor_lt (iff.mp !lt_neg_iff_lt_neg Hz),
+    note Hz' := lt_of_floor_lt (iff.mp !lt_neg_iff_lt_neg Hz),
     rewrite [of_int_neg at Hz'],
     apply lt_of_neg_lt_neg Hz'
   end
@@ -482,10 +482,10 @@ theorem floor_succ (x : ℝ) : floor (x + 1) = floor x + 1 :=
     apply by_contradiction,
     intro H,
     cases lt_or_gt_of_ne H with [Hgt, Hlt],
-    let Hl := lt_of_floor_lt Hgt,
+    note Hl := lt_of_floor_lt Hgt,
     rewrite [of_int_add at Hl],
     apply not_le_of_gt (lt_of_add_lt_add_right Hl) !floor_le,
-    let Hl := lt_of_floor_lt (iff.mp !add_lt_iff_lt_sub_right Hlt),
+    note Hl := lt_of_floor_lt (iff.mp !add_lt_iff_lt_sub_right Hlt),
     rewrite [of_int_sub at Hl],
     apply not_le_of_gt (iff.mpr !add_lt_iff_lt_sub_right Hl) !floor_le
   end
@@ -844,7 +844,7 @@ private theorem regular_lemma (s : seq) (H : ∀ n i : ℕ+, i ≥ n → under_s
     intros,
     cases em (m ≤ n) with [Hm, Hn],
     apply regular_lemma_helper Hm H,
-    let T := regular_lemma_helper (pnat.le_of_lt (pnat.lt_of_not_le Hn)) H,
+    note T := regular_lemma_helper (pnat.le_of_lt (pnat.lt_of_not_le Hn)) H,
     rewrite [abs_sub at T, {n⁻¹ + _}add.comm at T],
     exact T
   end

library/data/real/division.lean

@@ -404,7 +404,7 @@ theorem inv_well_defined {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s
         s_inv Hs ≡ s_inv Ht :=
   if Hsep : sep s zero then
     (begin
-       let Hsept := sep_of_equiv_sep Hs Ht Heq Hsep,
+       note Hsept := sep_of_equiv_sep Hs Ht Heq Hsep,
        have Hm : smul t (s_inv Hs) ≡ smul s (s_inv Hs), begin
          apply mul_well_defined,
          repeat (assumption | apply reg_inv_reg),
@@ -462,15 +462,15 @@ theorem s_le_total {s t : seq} (Hs : regular s) (Ht : regular t) : s_le s t ∨
           intro m,
           apply by_contradiction,
           intro Hm,
-          let Hm' := lt_of_not_ge Hm,
+          note Hm' := lt_of_not_ge Hm,
-          let Hex'' := exists.intro m Hm',
+          note Hex'' := exists.intro m Hm',
           apply Hex Hex''
         end,
         apply H Hex'
       end,
       eapply exists.elim H',
       intro m Hm,
-      let Hm' := neg_lt_neg Hm,
+      note Hm' := neg_lt_neg Hm,
       rewrite neg_neg at Hm',
       apply s_nonneg_of_pos,
       rotate 1,

library/data/real/order.lean

@@ -236,7 +236,7 @@ theorem s_neg_add_eq_s_add_neg (s t : seq) : sneg (sadd s t) ≡ sadd (sneg s) (
 theorem equiv_cancel_middle {s t u : seq} (Hs : regular s) (Ht : regular t)
         (Hu : regular u) : sadd (sadd u t) (sneg (sadd u s)) ≡ sadd t (sneg s) :=
   begin
-    let Hz := zero_is_reg,
+    note Hz := zero_is_reg,
     apply equiv.trans,
     rotate 3,
     apply add_well_defined,
@@ -308,7 +308,7 @@ protected theorem le_trans {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu :
           (Lst : s_le s t) (Ltu : s_le t u) : s_le s u :=
   begin
     rewrite ↑s_le at *,
-    let Rz := zero_is_reg,
+    note Rz := zero_is_reg,
     have Hsum : nonneg (sadd (sadd u (sneg t)) (sadd t (sneg s))),
                 from rat_seq.add_nonneg_of_nonneg Ltu Lst,
     have H' : nonneg (sadd (sadd u (sadd (sneg t) t)) (sneg s)), begin
@@ -384,7 +384,7 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_
     cases Lst with [N, HN],
     let Rns := reg_neg_reg Hs,
     let Rtns := reg_add_reg Ht Rns,
-    let Habs := sub_le_of_abs_sub_le_right (Rtns N n),
+    note Habs := sub_le_of_abs_sub_le_right (Rtns N n),
     rewrite [sub_add_eq_sub_sub at Habs],
     exact (calc
       sadd t (sneg s) n ≥ sadd t (sneg s) N -  N⁻¹ - n⁻¹ : Habs
@@ -401,14 +401,14 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_
 theorem lt_of_le_and_sep {s t : seq} (Hs : regular s) (Ht : regular t) (H : s_le s t ∧ sep s t) :
         s_lt s t :=
   begin
-    let Le := and.left H,
+    note Le := and.left H,
     cases and.right H with [P, Hlt],
     exact P,
     rewrite [↑s_le at Le, ↑nonneg at Le, ↑s_lt at Hlt, ↑pos at Hlt],
     apply exists.elim Hlt,
     intro N HN,
     let LeN := Le N,
-    let HN' := (iff.mpr !neg_lt_neg_iff_lt) HN,
+    note HN' := (iff.mpr !neg_lt_neg_iff_lt) HN,
     rewrite [↑sadd at HN', ↑sneg at HN', neg_add at HN', neg_neg at HN', add.comm at HN'],
     let HN'' := not_le_of_gt HN',
     apply absurd LeN HN''
@@ -652,8 +652,8 @@ theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t)
 theorem s_mul_ge_zero_of_ge_zero {s t : seq} (Hs : regular s) (Ht : regular t)
         (Hzs : s_le zero s) (Hzt : s_le zero t) : s_le zero (smul s t) :=
   begin
-    let Hzs' := s_nonneg_of_ge_zero Hs Hzs,
+    note Hzs' := s_nonneg_of_ge_zero Hs Hzs,
-    let Htz' := s_nonneg_of_ge_zero Ht Hzt,
+    note Htz' := s_nonneg_of_ge_zero Ht Hzt,
     apply s_ge_zero_of_nonneg,
     rotate 1,
     apply s_mul_nonneg_of_nonneg,

library/init/tactic.lean

@@ -130,7 +130,7 @@ definition change (e : expr) : tactic := builtin
 
 definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
 
-definition lettac (id : identifier) (e : expr) : tactic := builtin
+definition notetac (id : identifier) (e : expr) : tactic := builtin
 
 definition constructor (k : option num)  : tactic := builtin
 definition fconstructor (k : option num) : tactic := builtin

library/theories/analysis/real_limit.lean

@@ -544,7 +544,7 @@ theorem pos_on_nbhd_of_cts_of_pos {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ
     exact and.left Hδ,
     intro y Hy,
     let Hy' := and.right Hδ y Hy,
-    let Hlt := sub_lt_of_abs_sub_lt_right Hy',
+    note Hlt := sub_lt_of_abs_sub_lt_right Hy',
     rewrite sub_self at Hlt,
     assumption
   end
@@ -560,7 +560,7 @@ theorem neg_on_nbhd_of_cts_of_neg {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ
     intro y Hy,
     let Hy' := and.right Hδ y Hy,
     let Hlt := sub_lt_of_abs_sub_lt_left Hy',
-    let Hlt' := lt_add_of_sub_lt_right Hlt,
+    note Hlt' := lt_add_of_sub_lt_right Hlt,
     rewrite [-sub_eq_add_neg at Hlt', sub_self at Hlt'],
     assumption
   end
@@ -780,7 +780,7 @@ theorem intermediate_value_incr_zero : ∃ c, a < c ∧ c < b ∧ f c = 0 :=
     intro Hxgt,
     have Hxgt' : b - x < δ, from sub_lt_of_sub_lt Hxgt,
     krewrite -(abs_of_pos (sub_pos_of_lt (and.left Hx))) at Hxgt',
-    let Hxgt'' := and.right Hδ _ Hxgt',
+    note Hxgt'' := and.right Hδ _ Hxgt',
     exact not_lt_of_ge (le_of_lt Hxgt'') (and.right Hx)},
     {exact sup_fn_interval}
   end

library/theories/number_theory/bezout.lean

@@ -57,7 +57,7 @@ gcd.induction x y
     assume npos : 0 < n,
     assume IH,
     begin
-      let H := egcd_of_pos m npos, esimp at H,
+      note H := egcd_of_pos m npos, esimp at H,
       rewrite H,
       esimp,
       rewrite [gcd_rec, -IH],

library/theories/number_theory/irrational_roots.lean

@@ -156,7 +156,7 @@ section
   have pnez : p ≠ 0, from
     (suppose p = 0,
       show false,
-        by let H := (pos_of_prime primep); rewrite this at H; exfalso; exact !lt.irrefl H),
+        by note H := (pos_of_prime primep); rewrite this at H; exfalso; exact !lt.irrefl H),
   assert agtz : a > 0, from pos_of_ne_zero
     (suppose a = 0,
       show false, using npos pnez, by revert peq; rewrite [this, zero_pow npos]; exact pnez),

src/emacs/lean-syntax.el

@@ -72,7 +72,7 @@
     "xrewrite" "krewrite" "blast" "simp" "esimp" "unfold" "change" "check_expr" "contradiction"
     "exfalso" "split" "existsi" "constructor" "fconstructor" "left" "right" "injection" "congruence" "reflexivity"
     "symmetry" "transitivity" "state" "induction" "induction_using" "fail" "append"
-    "substvars" "now" "with_options" "with_attributes" "with_attrs")
+    "substvars" "now" "with_options" "with_attributes" "with_attrs" "note")
   "lean tactics")
 (defconst lean-tactics-regexp
   (eval `(rx word-start (or ,@lean-tactics) word-end)))

src/frontends/lean/builtin_tactics.cpp

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/tactic/let_tactic.h"
+#include <library/let.h>
+#include <library/constants.h>
+#include "library/tactic/note_tactic.h"
 #include "library/tactic/generalize_tactic.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/parser.h"
@@ -43,10 +45,22 @@ static expr parse_rparen(parser &, unsigned, expr const * args, pos_info const &
 }
 
 static expr parse_let_tactic(parser & p, unsigned, expr const *, pos_info const & pos) {
+    auto id_pos     = p.pos();
     name id    = p.check_atomic_id_next("invalid 'let' tactic, identifier expected");
     p.check_token_next(get_assign_tk(), "invalid 'let' tactic, ':=' expected");
     expr value = p.parse_tactic_expr_arg();
-    return p.save_pos(mk_let_tactic_expr(id, value), pos);
+    // Register value as expandable local expr. Identical to let term parsing, but without surrounding mk_let.
+    value = p.save_pos(mk_let_value(value), id_pos);
+    p.add_local_expr(id, value);
+    // nothing to do, so return the id tactic
+    return p.save_pos(mk_constant(get_tactic_id_name()), pos);
+}
+
+static expr parse_note_tactic(parser & p, unsigned, expr const *, pos_info const & pos) {
+    name id    = p.check_atomic_id_next("invalid 'note' tactic, identifier expected");
+    p.check_token_next(get_assign_tk(), "invalid 'note' tactic, ':=' expected");
+    expr value = p.parse_tactic_expr_arg();
+    return p.save_pos(mk_note_tactic_expr(id, value), pos);
 }
 
 static expr parse_with_options_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
@@ -87,6 +101,7 @@ parse_table init_tactic_nud_table() {
     r = r.add({transition("unfold",          mk_ext_action(parse_unfold_tactic_expr))}, x0);
     r = r.add({transition("fold",            mk_ext_action(parse_fold_tactic_expr))}, x0);
     r = r.add({transition("let",             mk_ext_action(parse_let_tactic))}, x0);
+    r = r.add({transition("note",            mk_ext_action(parse_note_tactic))}, x0);
     r = r.add({transition("with_options",    mk_ext_action(parse_with_options_tactic_expr))}, x0);
     r = r.add({transition("with_attributes", mk_ext_action(parse_with_attributes_tactic_expr))}, x0);
     r = r.add({transition("with_attrs",      mk_ext_action(parse_with_attributes_tactic_expr))}, x0);

src/frontends/lean/token_table.cpp

@@ -96,7 +96,7 @@ void init_token_table(token_table & t) {
          {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
          {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0},
-         {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"with_options", 0}, {"with_attributes", 0}, {"with_attrs", 0},
+         {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"note", 0}, {"with_options", 0}, {"with_attributes", 0}, {"with_attrs", 0},
          {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"#tactic", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec}, {"abstract", g_max_prec},
          {"proof", g_max_prec}, {"qed", 0}, {"@@", g_max_prec}, {"@", g_max_prec},

src/library/constants.cpp

@@ -229,8 +229,8 @@ name const * g_tactic_identifier_list = nullptr;
 name const * g_tactic_interleave = nullptr;
 name const * g_tactic_intro = nullptr;
 name const * g_tactic_intros = nullptr;
-name const * g_tactic_lettac = nullptr;
 name const * g_tactic_none_expr = nullptr;
+name const * g_tactic_notetac = nullptr;
 name const * g_tactic_now = nullptr;
 name const * g_tactic_opt_expr = nullptr;
 name const * g_tactic_opt_expr_list = nullptr;
@@ -487,8 +487,8 @@ void initialize_constants() {
     g_tactic_interleave = new name{"tactic", "interleave"};
     g_tactic_intro = new name{"tactic", "intro"};
     g_tactic_intros = new name{"tactic", "intros"};
-    g_tactic_lettac = new name{"tactic", "lettac"};
     g_tactic_none_expr = new name{"tactic", "none_expr"};
+    g_tactic_notetac = new name{"tactic", "notetac"};
     g_tactic_now = new name{"tactic", "now"};
     g_tactic_opt_expr = new name{"tactic", "opt_expr"};
     g_tactic_opt_expr_list = new name{"tactic", "opt_expr_list"};
@@ -746,8 +746,8 @@ void finalize_constants() {
     delete g_tactic_interleave;
     delete g_tactic_intro;
     delete g_tactic_intros;
-    delete g_tactic_lettac;
     delete g_tactic_none_expr;
+    delete g_tactic_notetac;
     delete g_tactic_now;
     delete g_tactic_opt_expr;
     delete g_tactic_opt_expr_list;
@@ -1004,8 +1004,8 @@ name const & get_tactic_identifier_list_name() { return *g_tactic_identifier_lis
 name const & get_tactic_interleave_name() { return *g_tactic_interleave; }
 name const & get_tactic_intro_name() { return *g_tactic_intro; }
 name const & get_tactic_intros_name() { return *g_tactic_intros; }
-name const & get_tactic_lettac_name() { return *g_tactic_lettac; }
 name const & get_tactic_none_expr_name() { return *g_tactic_none_expr; }
+name const & get_tactic_notetac_name() { return *g_tactic_notetac; }
 name const & get_tactic_now_name() { return *g_tactic_now; }
 name const & get_tactic_opt_expr_name() { return *g_tactic_opt_expr; }
 name const & get_tactic_opt_expr_list_name() { return *g_tactic_opt_expr_list; }

src/library/constants.h

@@ -231,8 +231,8 @@ name const & get_tactic_identifier_list_name();
 name const & get_tactic_interleave_name();
 name const & get_tactic_intro_name();
 name const & get_tactic_intros_name();
-name const & get_tactic_lettac_name();
 name const & get_tactic_none_expr_name();
+name const & get_tactic_notetac_name();
 name const & get_tactic_now_name();
 name const & get_tactic_opt_expr_name();
 name const & get_tactic_opt_expr_list_name();

src/library/constants.txt

@@ -224,8 +224,8 @@ tactic.identifier_list
 tactic.interleave
 tactic.intro
 tactic.intros
-tactic.lettac
 tactic.none_expr
+tactic.notetac
 tactic.now
 tactic.opt_expr
 tactic.opt_expr_list

src/library/tactic/CMakeLists.txt

@@ -3,7 +3,7 @@ apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp
 exact_tactic.cpp generalize_tactic.cpp inversion_tactic.cpp
 whnf_tactic.cpp revert_tactic.cpp assert_tactic.cpp clear_tactic.cpp
 expr_to_tactic.cpp location.cpp rewrite_tactic.cpp util.cpp
-init_module.cpp change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp
+init_module.cpp change_tactic.cpp check_expr_tactic.cpp note_tactic.cpp
 contradiction_tactic.cpp exfalso_tactic.cpp constructor_tactic.cpp
 injection_tactic.cpp congruence_tactic.cpp relation_tactics.cpp
 induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp

src/library/tactic/init_module.cpp

@@ -21,7 +21,7 @@ Author: Leonardo de Moura
 #include "library/tactic/rewrite_tactic.h"
 #include "library/tactic/change_tactic.h"
 #include "library/tactic/check_expr_tactic.h"
-#include "library/tactic/let_tactic.h"
+#include "library/tactic/note_tactic.h"
 #include "library/tactic/contradiction_tactic.h"
 #include "library/tactic/exfalso_tactic.h"
 #include "library/tactic/constructor_tactic.h"
@@ -52,7 +52,7 @@ void initialize_tactic_module() {
     initialize_rewrite_tactic();
     initialize_change_tactic();
     initialize_check_expr_tactic();
-    initialize_let_tactic();
+    initialize_note_tactic();
     initialize_contradiction_tactic();
     initialize_exfalso_tactic();
     initialize_constructor_tactic();
@@ -78,7 +78,7 @@ void finalize_tactic_module() {
     finalize_constructor_tactic();
     finalize_exfalso_tactic();
     finalize_contradiction_tactic();
-    finalize_let_tactic();
+    finalize_note_tactic();
     finalize_check_expr_tactic();
     finalize_change_tactic();
     finalize_rewrite_tactic();

src/library/tactic/note_tactic.cpp

@@ -13,12 +13,12 @@ Author: Leonardo de Moura
 #include "library/tactic/expr_to_tactic.h"
 
 namespace lean {
-expr mk_let_tactic_expr(name const & id, expr const & e) {
+expr mk_note_tactic_expr(name const &id, expr const &e) {
-    return mk_app(mk_constant(get_tactic_lettac_name()),
+    return mk_app(mk_constant(get_tactic_notetac_name()),
                   mk_constant(id), e);
 }
 
-tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
+tactic note_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
     return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
             proof_state new_s = s;
             goals const & gs  = new_s.get_goals();
@@ -33,7 +33,7 @@ tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
             expr new_e; substitution new_subst; constraints cs;
             std::tie(new_e, new_subst, cs) = esc;
             if (cs)
-                throw_tactic_exception_if_enabled(s, "invalid 'let' tactic, fail to resolve generated constraints");
+                throw_tactic_exception_if_enabled(s, "invalid 'note' tactic, fail to resolve generated constraints");
             auto tc         = mk_type_checker(env, ngen.mk_child());
             expr new_e_type = tc->infer(new_e).first;
             expr new_local  = mk_local(ngen.next(), id, new_e_type, binder_info());
@@ -50,14 +50,14 @@ tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
         });
 }
 
-void initialize_let_tactic() {
+void initialize_note_tactic() {
-    register_tac(get_tactic_lettac_name(),
+    register_tac(get_tactic_notetac_name(),
                  [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
-                     name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'let' tactic, argument must be an identifier");
+                     name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'note' tactic, argument must be an identifier");
-                     check_tactic_expr(app_arg(e), "invalid 'let' tactic, argument must be an expression");
+                     check_tactic_expr(app_arg(e), "invalid 'note' tactic, argument must be an expression");
-                     return let_tactic(fn, id, get_tactic_expr_expr(app_arg(e)));
+                     return note_tactic(fn, id, get_tactic_expr_expr(app_arg(e)));
                  });
 }
-void finalize_let_tactic() {
+void finalize_note_tactic() {
 }
 }

src/library/tactic/note_tactic.h

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
-expr mk_let_tactic_expr(name const & id, expr const & e);
+expr mk_note_tactic_expr(name const &id, expr const &e);
-void initialize_let_tactic();
+void initialize_note_tactic();
-void finalize_let_tactic();
+void finalize_note_tactic();
 }

tests/lean/hott/670.hlean

@@ -16,7 +16,7 @@ by krewrite [to_right_inv e b]
 
 example (b : B) : g (f (g b)) = g b :=
 begin
-  let H := to_right_inv e b,
+  note H := to_right_inv e b,
   esimp at H,
   rewrite H
 end

tests/lean/interactive/alias.input.expected.out

@@ -8,7 +8,6 @@ bool.band_tt|∀ (a : bool), eq (bool.band a bool.tt) a
 bool.tt|bool
 bool.eq_tt_of_bnot_eq_ff|eq (bool.bnot ?a) bool.ff → eq ?a bool.tt
 bool.eq_ff_of_bnot_eq_tt|eq (bool.bnot ?a) bool.tt → eq ?a bool.ff
-tactic.lettac|tactic.identifier → tactic.expr → tactic
 bool.absurd_of_eq_ff_of_eq_tt|eq ?a bool.ff → eq ?a bool.tt → ?B
 bool.eq_tt_of_ne_ff|ne ?a bool.ff → eq ?a bool.tt
 tactic.with_attributes_tac|tactic.expr → tactic.identifier_list → tactic → tactic
@@ -28,7 +27,6 @@ bor_tt|∀ (a : bool), eq (bor a tt) tt
 band_tt|∀ (a : bool), eq (band a tt) a
 eq_tt_of_bnot_eq_ff|eq (bnot ?a) ff → eq ?a tt
 eq_ff_of_bnot_eq_tt|eq (bnot ?a) tt → eq ?a ff
-tactic.lettac|tactic.identifier → tactic.expr → tactic
 absurd_of_eq_ff_of_eq_tt|eq ?a ff → eq ?a tt → ?B
 eq_tt_of_ne_ff|ne ?a ff → eq ?a tt
 tactic.with_attributes_tac|tactic.expr → tactic.identifier_list → tactic → tactic

tests/lean/run/blast_cc8.lean

@@ -11,7 +11,7 @@ begin
   induction a with f₁ h₁,
   induction b with f₂ h₂,
   subst xs,
-  let e := to_set.inj h₂,
+  note e := to_set.inj h₂,
   subst e
 end
 

tests/lean/run/congr_tac2.lean

@@ -17,7 +17,7 @@ begin
   induction a with f₁ h₁,
   induction b with f₂ h₂,
   subst xs,
-  let e := to_set.inj h₂,
+  note e := to_set.inj h₂,
   subst e
 end
 

tests/lean/run/dep_subst.lean

@@ -23,6 +23,6 @@ begin
   induction fn₁ with fxs₁ h₁,
   induction fn₂ with fxs₂ h₂,
   subst xs,
-  let aux := to_set.inj h₂,
+  note aux := to_set.inj h₂,
   subst aux
 end

tests/lean/run/let_tac.lean

@@ -4,6 +4,8 @@ open algebra
 example (a b : Prop) : a → b → a ∧ b :=
 begin
   intro Ha, intro Hb,
+  let Ha' := Ha,
+  let Hb' := Hb,
   let aux := and.intro Ha Hb,
   exact aux
 end