feat(frontends/lean): simplify explicit version names

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

examples/lean/set.lean

@@ -18,7 +18,7 @@ Theorem SubsetTrans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆
 
 Definition transitive {A : Type} (R : A → A → Bool) := ∀ x y z, R x y ⇒ R y z ⇒ R x z
 
-Theorem SubsetTrans2 {A : Type} : transitive (subset::explicit A) :=
+Theorem SubsetTrans2 {A : Type} : transitive (@subset A) :=
    ForallIntro (λ s1, ForallIntro (λ s2, ForallIntro (λ s3,
       Discharge (λ H1, (Discharge (λ H2,
          SubsetTrans H1 H2)))))).

src/frontends/lean/frontend.cpp

@@ -7,11 +7,13 @@ Author: Leonardo de Moura
 #include <vector>
 #include <utility>
 #include <functional>
+#include <string>
 #include "util/thread.h"
 #include "util/map.h"
 #include "util/sstream.h"
 #include "util/exception.h"
 #include "util/name_map.h"
+#include "util/name_set.h"
 #include "kernel/environment.h"
 #include "kernel/expr_maps.h"
 #include "kernel/expr_sets.h"
@@ -52,6 +54,7 @@ struct lean_extension : public environment_extension {
     coercion_set          m_coercion_set; // Set of coercions
     expr_to_coercions     m_type_coercions; // mapping type -> list (to-type, function)
     unsigned              m_initial_size; // size of the environment after init_frontend was invoked
+    name_set              m_explicit_names; // set of explicit version of constants with implicit parameters
 
     lean_extension() {
         m_initial_size = 0;
@@ -305,6 +308,21 @@ struct lean_extension : public environment_extension {
         }
     }
 
+    static name mk_explicit_name(name const & n) {
+        if (n.is_anonymous()) {
+            throw exception("anonymous names cannot be used in definitions");
+        } else if (n.is_numeral()) {
+            return name(n, "explicit");
+        } else {
+            std::string new_name = "@";
+            new_name += n.get_string();
+            if (n.is_atomic())
+                return name(new_name);
+            else
+                return name(n.get_prefix(), new_name.c_str());
+        }
+    }
+
     void mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit, environment const & env) {
         if (env->has_children())
             throw exception(sstream() << "failed to mark implicit arguments, frontend object is read-only");
@@ -313,7 +331,7 @@ struct lean_extension : public environment_extension {
             throw exception(sstream() << "failed to mark implicit arguments, the object '" << n << "' is not a definition or postulate");
         if (has_implicit_arguments(n))
             throw exception(sstream() << "the object '" << n << "' already has implicit argument information associated with it");
-        name explicit_version(n, "explicit");
+        name explicit_version = mk_explicit_name(n);
         if (env->find_object(explicit_version))
             throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', the frontend already has an object named '" << explicit_version << "'");
         expr const & type = obj.get_type();
@@ -329,6 +347,7 @@ struct lean_extension : public environment_extension {
         std::vector<bool> v(implicit, implicit+sz);
         m_implicit_table[n] = mk_pair(v, explicit_version);
         expr body = mk_explicit_definition_body(type, n, 0, num_args);
+        m_explicit_names.insert(explicit_version);
         if (obj.is_axiom() || obj.is_theorem()) {
             env->add_theorem(explicit_version, type, body);
         } else {
@@ -376,7 +395,13 @@ struct lean_extension : public environment_extension {
     }
 
     bool is_explicit(name const & n) const {
-        return !n.is_atomic() && get_explicit_version(n.get_prefix()) == n;
+        if (m_explicit_names.find(n) != m_explicit_names.end())
+            return true;
+        lean_extension const * parent = get_parent();
+        if (parent)
+            return parent->is_explicit(n);
+        else
+            return false;
     }
 
     /**

src/frontends/lean/scanner.cpp

@@ -54,9 +54,10 @@ public:
 
         set('_',  'a');
         set('\'', 'a');
+        set('@', 'a');
 
         // characters that can be used to create ids of group b
-        for (unsigned char b : {'=', '<', '>', '@', '^', '|', '&', '~', '+', '-', '*', '/', '\\', '$', '%', '?', ';', '[', ']', '#'})
+        for (unsigned char b : {'=', '<', '>', '^', '|', '&', '~', '+', '-', '*', '/', '\\', '$', '%', '?', ';', '[', ']', '#'})
             set(b, 'b');
 
         // punctuation

src/tests/frontends/lean/frontend.cpp

@@ -187,7 +187,7 @@ static void tst11() {
     } catch (exception & ex) {
         std::cout << "Expected error: " << ex.what() << std::endl;
     }
-    env->add_var(name{"h", "explicit"}, Pi({A, Type()}, A >> (A >> A)));
+    env->add_var(name("@h"), Pi({A, Type()}, A >> (A >> A)));
     env->add_var("h", Pi({A, Type()}, A >> (A >> A)));
     try {
         mark_implicit_arguments(env, "h", {true, false, false});

tests/lean/abst.lean.expected.out

@@ -4,5 +4,5 @@
   Assumed: a
 Abst (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a)
   Set: lean::pp::implicit
-Abst::explicit ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) :
+@Abst ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) :
     (λ x : ℤ, a + x) == (λ x : ℤ, x + a)

tests/lean/bad2.lean.expected.out

@@ -10,4 +10,4 @@
   Defined: n5
   Set: lean::pp::coercion
   Set: lean::pp::implicit
-Definition n5 : list ℕ := cons::explicit ℕ 10 (nil::explicit ℕ)
+Definition n5 : list ℕ := @cons ℕ 10 (@nil ℕ)

tests/lean/bug.lean.expected.out

@@ -6,7 +6,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
     Destruct/Decompose
     A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≺ (Type U)
         (line: 1: pos: 44) Type of argument 1 must be convertible to the expected type in the application of
-            Symm::explicit
+            @Symm
         with arguments:
             ?M::0
             ?M::1
@@ -22,7 +22,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                     Destruct/Decompose
                     A : (Type U), A' : (Type U), H : A == A' ⊢ A == A' ≺ ?M::1 == ?M::2
                         (line: 1: pos: 44) Type of argument 4 must be convertible to the expected type in the application of
-                            Symm::explicit
+                            @Symm
                         with arguments:
                             ?M::0
                             ?M::1
@@ -35,7 +35,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                 Substitution
                 A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0
                     (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of
-                        Symm::explicit
+                        @Symm
                     with arguments:
                         ?M::0
                         ?M::1
@@ -73,7 +73,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                 Substitution
                 A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0
                     (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of
-                        Symm::explicit
+                        @Symm
                     with arguments:
                         ?M::0
                         ?M::1
@@ -114,7 +114,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                     Destruct/Decompose
                     A : (Type U), A' : (Type U), H : A == A' ⊢ A == A' ≺ ?M::1 == ?M::2
                         (line: 1: pos: 44) Type of argument 4 must be convertible to the expected type in the application of
-                            Symm::explicit
+                            @Symm
                         with arguments:
                             ?M::0
                             ?M::1
@@ -127,7 +127,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                 Substitution
                 A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0
                     (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of
-                        Symm::explicit
+                        @Symm
                     with arguments:
                         ?M::0
                         ?M::1
@@ -165,7 +165,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                 Substitution
                 A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0
                     (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of
-                        Symm::explicit
+                        @Symm
                     with arguments:
                         ?M::0
                         ?M::1
@@ -206,7 +206,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                     Destruct/Decompose
                     A : (Type U), A' : (Type U), H : A == A' ⊢ A == A' ≺ ?M::1 == ?M::2
                         (line: 1: pos: 44) Type of argument 4 must be convertible to the expected type in the application of
-                            Symm::explicit
+                            @Symm
                         with arguments:
                             ?M::0
                             ?M::1
@@ -219,7 +219,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                 Substitution
                 A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0
                     (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of
-                        Symm::explicit
+                        @Symm
                     with arguments:
                         ?M::0
                         ?M::1
@@ -257,7 +257,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                 Substitution
                 A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0
                     (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of
-                        Symm::explicit
+                        @Symm
                     with arguments:
                         ?M::0
                         ?M::1
@@ -298,7 +298,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                     Destruct/Decompose
                     A : (Type U), A' : (Type U), H : A == A' ⊢ A == A' ≺ ?M::1 == ?M::2
                         (line: 1: pos: 44) Type of argument 4 must be convertible to the expected type in the application of
-                            Symm::explicit
+                            @Symm
                         with arguments:
                             ?M::0
                             ?M::1
@@ -311,7 +311,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                 Substitution
                 A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0
                     (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of
-                        Symm::explicit
+                        @Symm
                     with arguments:
                         ?M::0
                         ?M::1
@@ -349,7 +349,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                 Substitution
                 A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0
                     (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of
-                        Symm::explicit
+                        @Symm
                     with arguments:
                         ?M::0
                         ?M::1
@@ -390,7 +390,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                     Destruct/Decompose
                     A : (Type U), A' : (Type U), H : A == A' ⊢ A == A' ≺ ?M::1 == ?M::2
                         (line: 1: pos: 44) Type of argument 4 must be convertible to the expected type in the application of
-                            Symm::explicit
+                            @Symm
                         with arguments:
                             ?M::0
                             ?M::1
@@ -403,7 +403,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                 Substitution
                 A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0
                     (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of
-                        Symm::explicit
+                        @Symm
                     with arguments:
                         ?M::0
                         ?M::1
@@ -441,7 +441,7 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
                 Substitution
                 A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::5 ≺ ?M::0
                     (line: 1: pos: 44) Type of argument 3 must be convertible to the expected type in the application of
-                        Symm::explicit
+                        @Symm
                     with arguments:
                         ?M::0
                         ?M::1

tests/lean/cast2.lean.expected.out

@@ -9,5 +9,5 @@
 DomInj H : A == A'
   Proved: BeqB'
   Set: lean::pp::implicit
-DomInj::explicit A A' (λ x : A, B) (λ x : A', B') H
+@DomInj A A' (λ x : A, B) (λ x : A', B') H
-RanInj::explicit A A' (λ x : A, B) (λ x : A', B') H a
+@RanInj A A' (λ x : A, B) (λ x : A', B') H a

tests/lean/conv.lean

@@ -1,6 +1,3 @@
-
-
-
 Definition id (A : Type) : (Type U) := A.
 Variable p : (Int -> Int) -> Bool.
 Check fun (x : id Int), x.
@@ -14,7 +11,7 @@ Check g a.
 
 Definition c2 {T : Type} (A : (Type 3)) (a : T) : (Type 3) := (Type 1)
 Variable b : Int
-Check c2::explicit
+Check @c2
 Variable g2 : (c2 (Type 2) b) -> Bool
 Check g2
 Variable a2 : (c2 (Type 1) b).

tests/lean/conv.lean.expected.out

@@ -11,7 +11,7 @@ p f : Bool
 g a : Bool
   Defined: c2
   Assumed: b
-c2::explicit : Π (T : Type), (Type 3) → T → (Type 3)
+@c2 : Π (T : Type), (Type 3) → T → (Type 3)
   Assumed: g2
 g2 : c2 (Type 2) b → Bool
   Assumed: a2

tests/lean/elab1.lean.expected.out

@@ -10,7 +10,7 @@ Failed to solve
         Substitution
          ⊢ Bool ≺ ?M::0
             (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
-                f::explicit
+                @f
             with arguments:
                 ?M::0
                 ?M::1 10
@@ -20,7 +20,7 @@ Failed to solve
                 Substitution
                  ⊢ ?M::5[inst:0 (10)] ≺ ?M::0
                     (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
-                        f::explicit
+                        @f
                     with arguments:
                         ?M::0
                         ?M::1 10
@@ -44,7 +44,7 @@ Failed to solve
         Substitution
          ⊢ Bool ≺ ?M::0
             (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
-                f::explicit
+                @f
             with arguments:
                 ?M::0
                 ?M::1 10
@@ -54,7 +54,7 @@ Failed to solve
                 Substitution
                  ⊢ ?M::5[inst:0 (10)] ≺ ?M::0
                     (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
-                        f::explicit
+                        @f
                     with arguments:
                         ?M::0
                         ?M::1 10
@@ -78,7 +78,7 @@ Failed to solve
         Substitution
          ⊢ Bool ≺ ?M::0
             (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
-                f::explicit
+                @f
             with arguments:
                 ?M::0
                 ?M::1 10
@@ -88,7 +88,7 @@ Failed to solve
                 Substitution
                  ⊢ ?M::5[inst:0 (10)] ≺ ?M::0
                     (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
-                        f::explicit
+                        @f
                     with arguments:
                         ?M::0
                         ?M::1 10
@@ -142,7 +142,7 @@ Failed to solve
                 Destruct/Decompose
                  ⊢ Π H1 : ?M::2, ?M::3 ∧ ?M::4 ≺ Π a : ?M::0, ?M::1
                     (line: 20: pos: 18) Type of argument 3 must be convertible to the expected type in the application of
-                        Discharge::explicit
+                        @Discharge
                     with arguments:
                         ?M::0
                         ?M::1
@@ -152,7 +152,7 @@ Failed to solve
                     Substitution
                     H1 : ?M::2 ⊢ ?M::5 ≺ ?M::4
                         (line: 20: pos: 37) Type of argument 4 must be convertible to the expected type in the application of
-                            Conj::explicit
+                            @Conj
                         with arguments:
                             ?M::3
                             ?M::4
@@ -163,7 +163,7 @@ Failed to solve
                             Destruct/Decompose
                             H1 : ?M::2 ⊢ a ∧ b ≺ ?M::5 ∧ ?M::6
                                 (line: 20: pos: 45) Type of argument 3 must be convertible to the expected type in the application of
-                                    Conjunct1::explicit
+                                    @Conjunct1
                                 with arguments:
                                     ?M::5
                                     ?M::6
@@ -175,7 +175,7 @@ Failed to solve
         Destruct/Decompose
          ⊢ b == b ≺ ?M::3 == ?M::4
             (line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of
-                Trans::explicit
+                @Trans
             with arguments:
                 ?M::1
                 ?M::2
@@ -188,7 +188,7 @@ Failed to solve
             Destruct/Decompose
              ⊢ a == a ≺ ?M::2 == ?M::3
                 (line: 22: pos: 22) Type of argument 5 must be convertible to the expected type in the application of
-                    Trans::explicit
+                    @Trans
                 with arguments:
                     ?M::1
                     ?M::2
@@ -201,7 +201,7 @@ Failed to solve
     Destruct/Decompose
      ⊢ ?M::1 ≺ Type
         (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
-            f::explicit
+            @f
         with arguments:
             ?M::0
             Bool
@@ -211,7 +211,7 @@ Failed to solve
         Destruct/Decompose
          ⊢ Type ≺ ?M::0
             (line: 24: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
-                f::explicit
+                @f
             with arguments:
                 ?M::0
                 Bool
@@ -265,7 +265,7 @@ Failed to solve
         Destruct/Decompose
          ⊢ Type ≺ ?M::0
             (line: 24: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
-                f::explicit
+                @f
             with arguments:
                 ?M::0
                 Bool
@@ -323,7 +323,7 @@ a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ a
             Destruct/Decompose
             a : Bool, b : Bool, H : ?M::2 ⊢ Π H_a : ?M::6, ?M::2[lift:0:2] ≺ Π a : ?M::3, ?M::5[lift:0:1]
                 (line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of
-                    DisjCases::explicit
+                    @DisjCases
                 with arguments:
                     ?M::3
                     ?M::4
@@ -338,7 +338,7 @@ a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ a
                     Destruct/Decompose
                     a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1]
                         (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
-                            Discharge::explicit
+                            @Discharge
                         with arguments:
                             ?M::0
                             ?M::1
@@ -359,7 +359,7 @@ a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ a
                 Destruct/Decompose
                 a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1]
                     (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
-                        Discharge::explicit
+                        @Discharge
                     with arguments:
                         ?M::0
                         ?M::1

tests/lean/elab4.lean.expected.out

@@ -5,14 +5,10 @@
   Assumed: R
   Proved: R2
   Set: lean::pp::implicit
-Variable C {A B : Type} (H : eq::explicit Type A B) (a : A) : B
+Variable C {A B : Type} (H : @eq Type A B) (a : A) : B
-Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x)) :
+Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) :
-    eq::explicit Type A A'
+    @eq Type A A'
-Variable R {A A' : Type}
+Variable R {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) (a : A) :
-    {B : A → Type}
+    @eq Type (B a) (B' (@C A A' (@D A A' (λ x : A, B x) (λ x : A', B' x) H) a))
-    {B' : A' → Type}
+Theorem R2 (A1 A2 B1 B2 : Type) (H : @eq Type (A1 → B1) (A2 → B2)) (a : A1) : @eq Type B1 B2 :=
-    (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x))
+    @R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a
-    (a : A) :
-    eq::explicit Type (B a) (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
-Theorem R2 (A1 A2 B1 B2 : Type) (H : eq::explicit Type (A1 → B1) (A2 → B2)) (a : A1) : eq::explicit Type B1 B2 :=
-    R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a

tests/lean/elab5.lean.expected.out

@@ -5,14 +5,10 @@
   Assumed: R
   Proved: R2
   Set: lean::pp::implicit
-Variable C {A B : Type} (H : eq::explicit Type A B) (a : A) : B
+Variable C {A B : Type} (H : @eq Type A B) (a : A) : B
-Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x)) :
+Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) :
-    eq::explicit Type A A'
+    @eq Type A A'
-Variable R {A A' : Type}
+Variable R {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) (a : A) :
-    {B : A → Type}
+    @eq Type (B a) (B' (@C A A' (@D A A' (λ x : A, B x) (λ x : A', B' x) H) a))
-    {B' : A' → Type}
+Theorem R2 (A1 A2 B1 B2 : Type) (H : @eq Type (A1 → B1) (A2 → B2)) (a : A1) : @eq Type B1 B2 :=
-    (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x))
+    @R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a
-    (a : A) :
-    eq::explicit Type (B a) (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
-Theorem R2 (A1 A2 B1 B2 : Type) (H : eq::explicit Type (A1 → B1) (A2 → B2)) (a : A1) : eq::explicit Type B1 B2 :=
-    R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a

tests/lean/elab7.lean.expected.out

@@ -22,31 +22,23 @@ Theorem T3 : F1 = (λ (x1 : A) (x2 : B), F2 x1 x2) := Abst (λ a : A, Abst (λ b
 Theorem T4 : (λ (x1 : A) (x2 : B), F1 x1 x2) = (λ (x1 : A) (x2 : B), F2 x1 x2) :=
     Abst (λ a : A, Abst (λ b : B, H a b))
   Set: lean::pp::implicit
-Theorem T1 : eq::explicit (A → B → C) F1 F2 :=
+Theorem T1 : @eq (A → B → C) F1 F2 :=
-    Abst::explicit
+    @Abst A (λ x : A, B → C) F1 F2 (λ a : A, @Abst B (λ x : B, C) (F1 a) (F2 a) (λ b : B, H a b))
-        A
+Theorem T2 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) F2 :=
-        (λ x : A, B → C)
+    @Abst A
-        F1
+          (λ x : A, B → C)
-        F2
+          (λ (x1 : A) (x2 : B), F1 x1 x2)
-        (λ a : A, Abst::explicit B (λ x : B, C) (F1 a) (F2 a) (λ b : B, H a b))
+          F2
-Theorem T2 : eq::explicit (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) F2 :=
+          (λ a : A, @Abst B (λ x : B, C) (λ x2 : B, F1 a x2) (F2 a) (λ b : B, H a b))
-    Abst::explicit
+Theorem T3 : @eq (A → B → C) F1 (λ (x1 : A) (x2 : B), F2 x1 x2) :=
-        A
+    @Abst A
-        (λ x : A, B → C)
+          (λ x : A, B → C)
-        (λ (x1 : A) (x2 : B), F1 x1 x2)
+          F1
-        F2
+          (λ (x1 : A) (x2 : B), F2 x1 x2)
-        (λ a : A, Abst::explicit B (λ x : B, C) (λ x2 : B, F1 a x2) (F2 a) (λ b : B, H a b))
+          (λ a : A, @Abst B (λ x : B, C) (F1 a) (λ x2 : B, F2 a x2) (λ b : B, H a b))
-Theorem T3 : eq::explicit (A → B → C) F1 (λ (x1 : A) (x2 : B), F2 x1 x2) :=
+Theorem T4 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) (λ (x1 : A) (x2 : B), F2 x1 x2) :=
-    Abst::explicit
+    @Abst A
-        A
+          (λ x : A, B → C)
-        (λ x : A, B → C)
+          (λ (x1 : A) (x2 : B), F1 x1 x2)
-        F1
+          (λ (x1 : A) (x2 : B), F2 x1 x2)
-        (λ (x1 : A) (x2 : B), F2 x1 x2)
+          (λ a : A, @Abst B (λ x : B, C) (λ x2 : B, F1 a x2) (λ x2 : B, F2 a x2) (λ b : B, H a b))
-        (λ a : A, Abst::explicit B (λ x : B, C) (F1 a) (λ x2 : B, F2 a x2) (λ b : B, H a b))
-Theorem T4 : eq::explicit (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) (λ (x1 : A) (x2 : B), F2 x1 x2) :=
-    Abst::explicit
-        A
-        (λ x : A, B → C)
-        (λ (x1 : A) (x2 : B), F1 x1 x2)
-        (λ (x1 : A) (x2 : B), F2 x1 x2)
-        (λ a : A, Abst::explicit B (λ x : B, C) (λ x2 : B, F1 a x2) (λ x2 : B, F2 a x2) (λ b : B, H a b))

tests/lean/eq2.lean.expected.out

@@ -6,4 +6,4 @@
   Assumed: l
 l = nil : Bool
   Set: lean::pp::implicit
-eq::explicit (List ℤ) l (nil::explicit ℤ) : Bool
+@eq (List ℤ) l (@nil ℤ) : Bool

tests/lean/eq3.lean.expected.out

@@ -9,4 +9,4 @@
   Assumed: H2
 TransExt H1 H2 : v1 == v3
   Set: lean::pp::implicit
-TransExt::explicit (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3
+@TransExt (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3

tests/lean/ex3.lean.expected.out

@@ -29,7 +29,7 @@ Failed to solve
     Substitution
      ⊢ Bool ≺ ?M::0
         (line: 9: pos: 15) Type of argument 2 must be convertible to the expected type in the application of
-            myeq2::explicit
+            @myeq2
         with arguments:
             ?M::0
             ⊤
@@ -37,7 +37,7 @@ Failed to solve
         Assignment
          ⊢ T ≺ ?M::0
             (line: 9: pos: 15) Type of argument 3 must be convertible to the expected type in the application of
-                myeq2::explicit
+                @myeq2
             with arguments:
                 ?M::0
                 ⊤

tests/lean/exists4.lean

@@ -3,9 +3,9 @@ Variables a b c : N
 Variables P : N -> N -> N -> Bool
 Axiom H3 : P a b c
 
-Theorem T1 : exists x y z : N, P x y z := ExistsIntro::explicit N (fun x : N, exists y z : N, P x y z) a
+Theorem T1 : exists x y z : N, P x y z := @ExistsIntro N (fun x : N, exists y z : N, P x y z) a
-                                              (ExistsIntro::explicit N _ b
+                                              (@ExistsIntro N _ b
-                                                 (ExistsIntro::explicit N (fun z : N, P a b z) c H3))
+                                                 (@ExistsIntro N (fun z : N, P a b z) c H3))
 
 Theorem T2 : exists x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))
 

tests/lean/exists4.lean.expected.out

@@ -11,15 +11,11 @@
   Proved: T3
   Proved: T4
 Theorem T1 : ∃ x y z : N, P x y z :=
-    ExistsIntro::explicit
+    @ExistsIntro
         N
         (λ x : N, ∃ y z : N, P x y z)
         a
-        (ExistsIntro::explicit
+        (@ExistsIntro N (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1) b (@ExistsIntro N (λ z : N, P a b z) c H3))
-             N
-             (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1)
-             b
-             (ExistsIntro::explicit N (λ z : N, P a b z) c H3))
 Theorem T2 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))
 Theorem T3 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))
 Theorem T4 (H : P a a b) : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro a (ExistsIntro b H))

tests/lean/explicit.lean

@@ -0,0 +1,8 @@
+Variable f {A : Type} : A -> A -> A
+Variable module::g {A : Type} : A -> A -> A
+Check @f
+Check module::@g
+Variable h::1 {A B : Type} : A -> B -> A
+Check h::1::explicit
+Variable @h : Int -> Int
+Variable h {A B : Type} : A -> B -> A

tests/lean/explicit.lean.expected.out

@@ -0,0 +1,11 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+  Assumed: module::g
+@f : Π (A : Type), A → A → A
+module::@g : Π (A : Type), A → A → A
+  Assumed: h::1
+h::1::explicit : Π (A B : Type), A → B → A
+  Assumed: @h
+  Assumed: h
+Error (line: 8, pos: 37) failed to mark implicit arguments for 'h', the frontend already has an object named '@h'

tests/lean/implicit2.lean

@@ -1,7 +1,7 @@
 Variable f {A : Type} (x y : A) : A
 Check f 10 20
 Check f 10
-Check f::explicit
+Check @f
 Variable g {A : Type} (x1 x2 : A) {B : Type} (y1 y2 : B) : B
 Check g 10 20 true
 Check let r : Real -> Real -> Real := g 10 20

tests/lean/implicit2.lean.expected.out

@@ -3,10 +3,10 @@
   Assumed: f
 f 10 20 : ℕ
 f 10 : ℕ → ℕ
-f::explicit : Π (A : Type), A → A → A
+@f : Π (A : Type), A → A → A
   Assumed: g
 g 10 20 ⊤ : Bool → Bool
 let r : ℝ → ℝ → ℝ := g 10 20 in r : ℝ → ℝ → ℝ
 Error (line: 10, pos: 0) invalid expression, unexpected token
   Set: lean::pp::implicit
-let r : ℝ → ℝ → ℝ := g::explicit ℕ 10 20 ℝ in r : ℝ → ℝ → ℝ
+let r : ℝ → ℝ → ℝ := @g ℕ 10 20 ℝ in r : ℝ → ℝ → ℝ

tests/lean/implicit4.lean.expected.out

@@ -7,5 +7,5 @@
 The denotation(s) for the existing notation:
   Infix ++
 have been replaced with the new denotation:
-  h::explicit
+  @h
 because they conflict on how implicit arguments are used.

tests/lean/implicit5.lean.expected.out

@@ -8,5 +8,5 @@
 The denotation(s) for the existing notation:
   Infix ++
 have been replaced with the new denotation:
-  p2::explicit
+  @p2
 because they conflict on how implicit arguments are used.

tests/lean/implicit7.lean.expected.out

@@ -8,5 +8,5 @@
 g 10 ⊤ ⊥ : Bool
 f 10 10 ⊤ : ℕ
   Set: lean::pp::implicit
-g::explicit ℕ Bool 10 Bool ⊤ ⊥ : Bool
+@g ℕ Bool 10 Bool ⊤ ⊥ : Bool
-f::explicit ℕ 10 Bool 10 ⊤ : ℕ
+@f ℕ 10 Bool 10 ⊤ : ℕ

tests/lean/subst.lean.expected.out

@@ -8,5 +8,5 @@
   Set: lean::pp::coercion
   Set: lean::pp::notation
   Set: lean::pp::implicit
-Theorem T : eq::explicit ℤ (Int::add (Int::add a (nat_to_int n)) a) (nat_to_int 10) :=
+Theorem T : @eq ℤ (Int::add (Int::add a (nat_to_int n)) a) (nat_to_int 10) :=
-    Subst::explicit ℤ a (nat_to_int n) (λ x : ℤ, Int::add (Int::add a x) a == nat_to_int 10) H1 H2
+    @Subst ℤ a (nat_to_int n) (λ x : ℤ, Int::add (Int::add a x) a == nat_to_int 10) H1 H2

tests/lean/tst1.lean

@@ -17,10 +17,10 @@ Check select (update (const three false) two true) two two_lt_three
 Eval select (update (const three false) two true) two two_lt_three
 Check update (const three false) two true
 Echo "\n--------"
-Check select::explicit
+Check @select
 Echo "\nmap type ---> "
-Check map::explicit
+Check @map
 Echo "\nmap normal form --> "
-Eval map::explicit
+Eval @map
 Echo "\nupdate normal form --> "
-Eval update::explicit
+Eval @update

tests/lean/tst1.lean.expected.out

@@ -29,10 +29,10 @@ if (two == two) ⊤ ⊥
 update (const three ⊥) two ⊤ : vector Bool three
 
 --------
-select::explicit : Π (A : Type) (n : N) (v : vector A n) (i : N), i < n → A
+@select : Π (A : Type) (n : N) (v : vector A n) (i : N), i < n → A
 
 map type ---> 
-map::explicit : Π (A B C : Type) (n : N), (A → B → C) → vector A n → vector B n → vector C n
+@map : Π (A B C : Type) (n : N), (A → B → C) → vector A n → vector B n → vector C n
 
 map normal form --> 
 λ (A B C : Type)

tests/lean/tst10.lean

@@ -21,6 +21,6 @@ Eval true => a
 (* Simple proof *)
 Axiom H1 : a
 Axiom H2 : a => b
-Check MP::explicit
+Check @MP
 Show MP H2 H1
 Check MP H2 H1

tests/lean/tst10.lean.expected.out

@@ -19,6 +19,6 @@ if a a ⊤
 a
   Assumed: H1
   Assumed: H2
-MP::explicit : Π (a b : Bool), (a ⇒ b) → a → b
+@MP : Π (a b : Bool), (a ⇒ b) → a → b
 MP H2 H1
 MP H2 H1 : b

tests/lean/tst11.lean

@@ -5,7 +5,7 @@ Eval xor true true
 Eval xor true false
 Variable a : Bool
 Show a ⊕ a ⊕ a
-Check Subst::explicit
+Check @Subst
 Theorem EM2 (a : Bool) : a \/ (not a) :=
    Case (fun x : Bool, x \/ (not x)) Trivial Trivial a
 Check EM2

tests/lean/tst11.lean.expected.out

@@ -6,7 +6,7 @@
 ⊤
   Assumed: a
 a ⊕ a ⊕ a
-Subst::explicit : Π (A : (Type U)) (a b : A) (P : A → Bool), P a → a == b → P b
+@Subst : Π (A : (Type U)) (a b : A) (P : A → Bool), P a → a == b → P b
   Proved: EM2
 EM2 : Π a : Bool, a ∨ ¬ a
 EM2 a : a ∨ ¬ a

tests/lean/tst4.lean

@@ -9,7 +9,7 @@ Variable EqNice {A : Type} (lhs rhs : A) : Bool
 Infix 50 === : EqNice
 Show n1 === n2
 Check f n1 n2
-Check Congr::explicit
+Check @Congr
 Show f n1 n2
 Variable a : N
 Variable b : N

tests/lean/tst4.lean.expected.out

@@ -5,34 +5,26 @@
   Assumed: n1
   Assumed: n2
   Set: lean::pp::implicit
-f::explicit N n1 n2
+@f N n1 n2
-f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
+@f ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
   Assumed: EqNice
-EqNice::explicit N n1 n2
+@EqNice N n1 n2
-f::explicit N n1 n2 : N
+@f N n1 n2 : N
-Congr::explicit :
+@Congr : Π (A : (Type U)) (B : A → (Type U)) (f g : Π x : A, B x) (a b : A), f == g → a == b → f a == g b
-    Π (A : (Type U)) (B : A → (Type U)) (f g : Π x : A, B x) (a b : A), f == g → a == b → f a == g b
+@f N n1 n2
-f::explicit N n1 n2
   Assumed: a
   Assumed: b
   Assumed: c
   Assumed: g
   Assumed: H1
   Proved: Pr
-Axiom H1 : eq::explicit N a b ∧ eq::explicit N b c
+Axiom H1 : @eq N a b ∧ @eq N b c
-Theorem Pr : eq::explicit N (g a) (g c) :=
+Theorem Pr : @eq N (g a) (g c) :=
-    Congr::explicit
+    @Congr N
-        N
+           (λ x : N, N)
-        (λ x : N, N)
+           g
-        g
+           g
-        g
+           a
-        a
+           c
-        c
+           (@Refl (N → N) g)
-        (Refl::explicit (N → N) g)
+           (@Trans N a b c (@Conjunct1 (@eq N a b) (@eq N b c) H1) (@Conjunct2 (@eq N a b) (@eq N b c) H1))
-        (Trans::explicit
-             N
-             a
-             b
-             c
-             (Conjunct1::explicit (eq::explicit N a b) (eq::explicit N b c) H1)
-             (Conjunct2::explicit (eq::explicit N a b) (eq::explicit N b c) H1))

tests/lean/tst5.lean.expected.out

@@ -6,6 +6,6 @@
 a = b
 a = b : Bool
   Set: lean::pp::implicit
-eq::explicit N a b
+@eq N a b
-eq::explicit (Type 2) (Type 1) (Type 1)
+@eq (Type 2) (Type 1) (Type 1)
-eq::explicit Bool ⊤ ⊥
+@eq Bool ⊤ ⊥

tests/lean/tst6.lean.expected.out

@@ -5,102 +5,55 @@
   Proved: CongrH
   Set: lean::pp::implicit
 Variable h : N → N → N
-Theorem CongrH {a1 a2 b1 b2 : N} (H1 : eq::explicit N a1 b1) (H2 : eq::explicit N a2 b2) : eq::explicit
+Theorem CongrH {a1 a2 b1 b2 : N} (H1 : @eq N a1 b1) (H2 : @eq N a2 b2) : @eq N (h a1 a2) (h b1 b2) :=
-        N
+    @Congr N (λ x : N, N) (h a1) (h b1) a2 b2 (@Congr N (λ x : N, N → N) h h a1 b1 (@Refl (N → N → N) h) H1) H2
-        (h a1 a2)
-        (h b1 b2) :=
-    Congr::explicit
-        N
-        (λ x : N, N)
-        (h a1)
-        (h b1)
-        a2
-        b2
-        (Congr::explicit N (λ x : N, N → N) h h a1 b1 (Refl::explicit (N → N → N) h) H1)
-        H2
   Set: lean::pp::implicit
 Variable h : N → N → N
 Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 b2 := Congr (Congr (Refl h) H1) H2
   Proved: Example1
   Set: lean::pp::implicit
-Theorem Example1 (a b c d : N)
+Theorem Example1 (a b c d : N) (H : @eq N a b ∧ @eq N b c ∨ @eq N a d ∧ @eq N d c) : @eq N (h a b) (h c b) :=
-    (H : eq::explicit N a b ∧ eq::explicit N b c ∨ eq::explicit N a d ∧ eq::explicit N d c) : eq::explicit
+    @DisjCases
-        N
+        (@eq N a b ∧ @eq N b c)
-        (h a b)
+        (@eq N a d ∧ @eq N d c)
-        (h c b) :=
-    DisjCases::explicit
-        (eq::explicit N a b ∧ eq::explicit N b c)
-        (eq::explicit N a d ∧ eq::explicit N d c)
         (h a b == h c b)
         H
-        (λ H1 : eq::explicit N a b ∧ eq::explicit N b c,
+        (λ H1 : @eq N a b ∧ @eq N b c,
-           CongrH::explicit
+           @CongrH a
-               a
+                   b
-               b
+                   c
-               c
+                   b
-               b
+                   (@Trans N a b c (@Conjunct1 (@eq N a b) (@eq N b c) H1) (@Conjunct2 (@eq N a b) (@eq N b c) H1))
-               (Trans::explicit
+                   (@Refl N b))
-                    N
+        (λ H1 : @eq N a d ∧ @eq N d c,
-                    a
+           @CongrH a
-                    b
+                   b
-                    c
+                   c
-                    (Conjunct1::explicit (eq::explicit N a b) (eq::explicit N b c) H1)
+                   b
-                    (Conjunct2::explicit (eq::explicit N a b) (eq::explicit N b c) H1))
+                   (@Trans N a d c (@Conjunct1 (@eq N a d) (@eq N d c) H1) (@Conjunct2 (@eq N a d) (@eq N d c) H1))
-               (Refl::explicit N b))
+                   (@Refl N b))
-        (λ H1 : eq::explicit N a d ∧ eq::explicit N d c,
-           CongrH::explicit
-               a
-               b
-               c
-               b
-               (Trans::explicit
-                    N
-                    a
-                    d
-                    c
-                    (Conjunct1::explicit (eq::explicit N a d) (eq::explicit N d c) H1)
-                    (Conjunct2::explicit (eq::explicit N a d) (eq::explicit N d c) H1))
-               (Refl::explicit N b))
   Proved: Example2
   Set: lean::pp::implicit
-Theorem Example2 (a b c d : N)
+Theorem Example2 (a b c d : N) (H : @eq N a b ∧ @eq N b c ∨ @eq N a d ∧ @eq N d c) : @eq N (h a b) (h c b) :=
-    (H : eq::explicit N a b ∧ eq::explicit N b c ∨ eq::explicit N a d ∧ eq::explicit N d c) : eq::explicit
+    @DisjCases
-        N
+        (@eq N a b ∧ @eq N b c)
-        (h a b)
+        (@eq N a d ∧ @eq N d c)
-        (h c b) :=
+        (@eq N (h a b) (h c b))
-    DisjCases::explicit
-        (eq::explicit N a b ∧ eq::explicit N b c)
-        (eq::explicit N a d ∧ eq::explicit N d c)
-        (eq::explicit N (h a b) (h c b))
         H
-        (λ H1 : eq::explicit N a b ∧ eq::explicit N b c,
+        (λ H1 : @eq N a b ∧ @eq N b c,
-           CongrH::explicit
+           @CongrH a
-               a
+                   b
-               b
+                   c
-               c
+                   b
-               b
+                   (@Trans N a b c (@Conjunct1 (a == b) (@eq N b c) H1) (@Conjunct2 (@eq N a b) (b == c) H1))
-               (Trans::explicit
+                   (@Refl N b))
-                    N
+        (λ H1 : @eq N a d ∧ @eq N d c,
-                    a
+           @CongrH a
-                    b
+                   b
-                    c
+                   c
-                    (Conjunct1::explicit (a == b) (eq::explicit N b c) H1)
+                   b
-                    (Conjunct2::explicit (eq::explicit N a b) (b == c) H1))
+                   (@Trans N a d c (@Conjunct1 (a == d) (@eq N d c) H1) (@Conjunct2 (@eq N a d) (d == c) H1))
-               (Refl::explicit N b))
+                   (@Refl N b))
-        (λ H1 : eq::explicit N a d ∧ eq::explicit N d c,
-           CongrH::explicit
-               a
-               b
-               c
-               b
-               (Trans::explicit
-                    N
-                    a
-                    d
-                    c
-                    (Conjunct1::explicit (a == d) (eq::explicit N d c) H1)
-                    (Conjunct2::explicit (eq::explicit N a d) (d == c) H1))
-               (Refl::explicit N b))
   Proved: Example3
   Set: lean::pp::implicit
 Theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : h a b = h c b :=