feat(frontends/lean/parser): allow 'typeless' definitions, the type is inferred by the system

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/parser.cpp

@@ -211,6 +211,8 @@ class parser::imp {
     bool curr_is_lcurly() const { return curr() == scanner::token::LeftCurlyBracket; }
     /** \brief Return true iff the current token is a ':' */
     bool curr_is_colon() const { return curr() == scanner::token::Colon; }
+    /** \brief Return true iff the current token is a ':=' */
+    bool curr_is_assign() const { return curr() == scanner::token::Assign; }
     /** \brief Return true iff the current token is an 'in' token */
     bool curr_is_in() const { return curr() == scanner::token::In; }
 
@@ -1039,6 +1041,11 @@ class parser::imp {
             pre_type = parse_expr();
             check_assign_next("invalid definition, ':=' expected");
             pre_val  = parse_expr();
+        } else if (is_definition && curr_is_assign()) {
+            auto p   = pos();
+            next();
+            pre_type = save(mk_placholder(), p);
+            pre_val  = parse_expr();
         } else {
             mk_scope scope(*this);
             parse_object_bindings(bindings);

tests/lean/revapp.lean

@@ -0,0 +1,29 @@
+Definition revapp {A : Type U} {B : A -> Type U} (a : A) (f : Pi (x : A), B x) : (B a) := f a.
+Infixl 100 |> : revapp
+
+Eval 10 |> (fun x, x + 1)
+        |> (fun x, x + 2)
+        |> (fun x, 2 * x)
+        |> (fun x, 3 - x)
+        |> (fun x, x + 2)
+
+Definition revcomp {A B C: Type U} (f : A -> B) (g : B -> C) : A -> C :=
+        fun x, g (f x)
+Infixl 100 #> : revcomp
+
+Eval (fun x, x + 1)     #>
+     (fun x, 2 * x * x) #>
+     (fun x, 10 + x)
+
+Definition simple := (fun x, x + 1)     #>
+                     (fun x, 2 * x * x) #>
+                     (fun x, 10 + x)
+
+Check simple
+Eval simple 10
+
+Definition simple2 := (fun x : Int, x + 1) #>
+                      (fun x, 2 * x * x)   #>
+                      (fun x, 10 + x)
+Check simple2
+Eval simple2 (-10)

tests/lean/revapp.lean.expected.out

@@ -0,0 +1,12 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Defined: revapp
+-21
+  Defined: revcomp
+λ x : ℕ, 10 + 2 * (x + 1) * (x + 1)
+  Defined: simple
+simple : ℕ → ℕ
+252
+  Defined: simple2
+simple2 : ℤ → ℤ
+172