From 4b91cfccff8653e5de2c8188de5d99158dbd134d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 10 Jun 2015 14:08:46 -0700
Subject: [PATCH] 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    | 6 ------
 hott/init/trunc.hlean                | 4 ++--
 hott/types/int/basic.hlean           | 2 +-
 library/data/int/basic.lean          | 2 +-
 library/init/reserved_notation.lean  | 6 ------
 src/frontends/lean/builtin_exprs.cpp | 5 +++++
 tests/lean/run/fun.lean              | 4 ++--
 7 files changed, 11 insertions(+), 18 deletions(-)

diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean
index abe7003d3..edad036d5 100644
--- a/hott/init/reserved_notation.hlean
+++ b/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
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index 31da9581c..5759be360 100644
--- a/hott/init/trunc.hlean
+++ b/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 -/
 
diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean
index 1295fc198..21bfdd81b 100644
--- a/hott/types/int/basic.hlean
+++ b/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)⁻¹)
 
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index e386b0733..034af64eb 100644
--- a/library/data/int/basic.lean
+++ b/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)⁻¹)
 
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index 6ded1f13f..8a25aa453 100644
--- a/library/init/reserved_notation.lean
+++ b/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
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index df0269988..6e5754c32 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/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);
diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean
index ebbc8195c..d312505a7 100644
--- a/tests/lean/run/fun.lean
+++ b/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