feat(frontends/lean/builtin_exprs): make notation ( e : T ) builtin

In the previous approach, the following (definitionally equal) term was being generated

       (fun (A : Type) (a : A), a) T e

hott/init/reserved_notation.hlean

@@ -92,9 +92,3 @@ reserve infixl `∪`:65
 reserve infix `∣`:50
 reserve infixl `++`:65
 reserve infixr `::`:65
-
--- Yet another trick to anotate an expression with a type
-abbreviation is_typeof [parsing-only] (A : Type) (a : A) : A := a
-
-notation `typeof` t `:` T  := is_typeof T t
-notation `(` t `:` T `)`  := is_typeof T t

hott/init/trunc.hlean

@@ -149,11 +149,11 @@ namespace is_trunc
 
   theorem is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A]
       : is_trunc (n.+1) A :=
-  is_trunc_of_leq A (star : -1 ≤ n.+1)
+  is_trunc_of_leq A (show -1 ≤ n.+1, from star)
 
   theorem is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A]
       : is_trunc (n.+2) A :=
-  is_trunc_of_leq A (star : 0 ≤ n.+2)
+  is_trunc_of_leq A (show 0 ≤ n.+2, from star)
 
   /- hprops -/
 

hott/types/int/basic.hlean

@@ -580,7 +580,7 @@ calc
     ... = a * b + c * a : {mul.comm b a}
     ... = a * b + a * c : {mul.comm c a}
 
-definition zero_ne_one : (typeof 0 : int) ≠ 1 :=
+definition zero_ne_one : (0 : int) ≠ 1 :=
 assume H : 0 = 1,
 show empty, from succ_ne_zero 0 ((of_nat.inj H)⁻¹)
 

library/data/int/basic.lean

@@ -585,7 +585,7 @@ calc
     ... = a * b + c * a : {mul.comm b a}
     ... = a * b + a * c : {mul.comm c a}
 
-theorem zero_ne_one : (typeof 0 : int) ≠ 1 :=
+theorem zero_ne_one : (0 : int) ≠ 1 :=
 assume H : 0 = 1,
 show false, from succ_ne_zero 0 ((of_nat.inj H)⁻¹)
 

library/init/reserved_notation.lean

@@ -93,9 +93,3 @@ reserve infix `⊆`:50
 reserve infix `∣`:50
 reserve infixl `++`:65
 reserve infixr `::`:65
-
--- Yet another trick to anotate an expression with a type
-abbreviation is_typeof [parsing-only] (A : Type) (a : A) : A := a
-
-notation `typeof` t `:` T  := is_typeof T t
-notation `(` t `:` T `)`  := is_typeof T t

src/frontends/lean/builtin_exprs.cpp

@@ -609,6 +609,10 @@ static expr parse_inaccessible(parser & p, unsigned, expr const * args, pos_info
     return p.save_pos(mk_inaccessible(args[0]), pos);
 }
 
+static expr parse_typed_expr(parser & p, unsigned, expr const * args, pos_info const & pos) {
+    return p.save_pos(mk_typed_expr(args[1], args[0]), pos);
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -624,6 +628,7 @@ parse_table init_nud_table() {
     r = r.add({transition("obtain", mk_ext_action(parse_obtain))}, x0);
     r = r.add({transition("if", mk_ext_action(parse_if_then_else))}, x0);
     r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0);
+    r = r.add({transition("(", Expr), transition(":", Expr), transition(")", mk_ext_action(parse_typed_expr))}, x0);
     r = r.add({transition("?(", Expr), transition(")", mk_ext_action(parse_inaccessible))}, x0);
     r = r.add({transition("⌞", Expr), transition("⌟", mk_ext_action(parse_inaccessible))}, x0);
     r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0);

tests/lean/run/fun.lean

@@ -7,14 +7,14 @@ constant g : num → num
 
 check f ∘ g ∘ g
 
-check typeof id : num → num
+check (id : num → num)
 
 constant h : num → bool → num
 
 check swap h
 check swap h ff num.zero
 
-check typeof swap h ff num.zero : num
+check (swap h ff num.zero : num)
 
 constant f1 : num → num → bool
 constant f2 : bool → num