Allow notation to be associated with arbitrary expression (instead of only constants).

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

examples/ex3.lean

@@ -1,5 +1,5 @@
 Definition xor (x y : Bool) : Bool := (not x) = y
-Infixr 50 ⊕ xor
+Infixr 50 ⊕ : xor
 Show xor true false
 Eval xor true true
 Eval xor true false

src/frontend/builtin_notation.cpp

@@ -12,16 +12,16 @@ namespace lean {
    \brief Initialize builtin notation.
 */
 void init_builtin_notation(frontend & f) {
-    f.add_prefix("\u00ac", 40, const_name(mk_not_fn()));
+    f.add_prefix("\u00ac", 40, mk_not_fn());
-    f.add_infixr("&&", 35, const_name(mk_and_fn()));
+    f.add_infixr("&&", 35, mk_and_fn());
-    f.add_infixr("/\\", 35, const_name(mk_and_fn()));
+    f.add_infixr("/\\", 35, mk_and_fn());
-    f.add_infixr("\u2227", 35, const_name(mk_and_fn()));
+    f.add_infixr("\u2227", 35, mk_and_fn());
-    f.add_infixr("||", 30, const_name(mk_or_fn()));
+    f.add_infixr("||", 30, mk_or_fn());
-    f.add_infixr("\\/", 30, const_name(mk_or_fn()));
+    f.add_infixr("\\/", 30, mk_or_fn());
-    f.add_infixr("\u2228", 30, const_name(mk_or_fn()));
+    f.add_infixr("\u2228", 30, mk_or_fn());
-    f.add_infixr("=>", 25, const_name(mk_implies_fn()));
+    f.add_infixr("=>", 25, mk_implies_fn());
-    f.add_infixr("\u21D2", 25, const_name(mk_implies_fn()));
+    f.add_infixr("\u21D2", 25, mk_implies_fn());
-    f.add_infixr("<=>", 25, const_name(mk_iff_fn()));
+    f.add_infixr("<=>", 25, mk_iff_fn());
-    f.add_infixr("\u21D4", 25, const_name(mk_iff_fn()));
+    f.add_infixr("\u21D4", 25, mk_iff_fn());
 }
 }

src/frontend/frontend.cpp

@@ -19,12 +19,13 @@ struct frontend::imp {
     // Remark: only named objects are stored in the dictionary.
     typedef std::unordered_map<name, operator_info, name_hash, name_eq> operator_table;
     typedef std::unordered_map<name, unsigned, name_hash, name_eq> implicit_table;
+    typedef std::unordered_map<expr, operator_info, expr_hash, std::equal_to<expr>> expr_to_operator;
     std::atomic<unsigned> m_num_children;
     std::shared_ptr<imp>  m_parent;
     environment           m_env;
     operator_table        m_nud; // nud table for Pratt's parser
     operator_table        m_led; // led table for Pratt's parser
-    operator_table        m_name_to_operator; // map internal names to operators (this is used for pretty printing)
+    expr_to_operator      m_expr_to_operator; // map denotations to operators (this is used for pretty printing)
     implicit_table        m_implicit_table; // track the number of implicit arguments for a symbol.
 
     bool has_children() const { return m_num_children > 0; }
@@ -79,13 +80,13 @@ struct frontend::imp {
             insert(m_nud, op.get_op_name(), op);
     }
 
-    /** \brief Find the operator that is used as notation for the given internal symbol. */
+    /** \brief Find the operator that is used as notation for the given expression. */
-    operator_info find_op_for(name const & n) const {
+    operator_info find_op_for(expr const & e) const {
-        auto it = m_name_to_operator.find(n);
+        auto it = m_expr_to_operator.find(e);
-        if (it != m_name_to_operator.end())
+        if (it != m_expr_to_operator.end())
             return it->second;
         else if (has_parent())
-            return m_parent->find_op_for(n);
+            return m_parent->find_op_for(e);
         else
             return operator_info();
     }
@@ -98,23 +99,23 @@ struct frontend::imp {
         // TODO
     }
 
-    /** \brief Remove all internal operators that are associated with the given operator symbol (aka notation) */
+    /** \brief Remove all internal denotations that are associated with the given operator symbol (aka notation) */
     void remove_bindings(operator_info const & op) {
-        for (name const & n : op.get_internal_names()) {
+        for (expr const & d : op.get_exprs()) {
-            if (has_parent() && m_parent->find_op_for(n)) {
+            if (has_parent() && m_parent->find_op_for(d)) {
-                // parent has a binding for n... we must hide it.
+                // parent has an association for d... we must hide it.
-                insert(m_name_to_operator, n, operator_info());
+                insert(m_expr_to_operator, d, operator_info());
             } else {
-                m_name_to_operator.erase(n);
+                m_expr_to_operator.erase(d);
             }
         }
     }
 
     /** \brief Register the new operator in the tables for parsing and pretty printing. */
-    void register_new_op(operator_info new_op, name const & n, bool led) {
+    void register_new_op(operator_info new_op, expr const & d, bool led) {
-        new_op.add_internal_name(n);
+        new_op.add_expr(d);
         insert_op(new_op, led);
-        insert(m_name_to_operator, n, new_op);
+        insert(m_expr_to_operator, d, new_op);
     }
 
     /**
@@ -128,37 +129,37 @@ struct frontend::imp {
         2) It is a real conflict, and report the issue in the
         diagnostic channel, and override the existing operator (aka notation).
     */
-    void add_op(operator_info new_op, name const & n, bool led) {
+    void add_op(operator_info new_op, expr const & d, bool led) {
         name const & opn = new_op.get_op_name();
         operator_info old_op = find_op(opn, led);
         if (!old_op) {
-            register_new_op(new_op, n, led);
+            register_new_op(new_op, d, led);
         } else if (old_op == new_op) {
             // overload
             if (defined_here(old_op, led)) {
-                old_op.add_internal_name(n);
+                old_op.add_expr(d);
             } else {
                 // we must copy the operator because it was defined in
                 // a parent frontend.
                 new_op = old_op.copy();
-                register_new_op(new_op, n, led);
+                register_new_op(new_op, d, led);
             }
         } else {
             report_op_redefined(old_op, new_op);
             remove_bindings(old_op);
-            register_new_op(new_op, n, led);
+            register_new_op(new_op, d, led);
         }
-        m_env.add_neutral_object(new notation_declaration(new_op, n));
+        m_env.add_neutral_object(new notation_declaration(new_op, d));
     }
 
-    void add_infix(name const & opn, unsigned p, name const & n)  { add_op(infix(opn, p), n, true); }
+    void add_infix(name const & opn, unsigned p, expr const & d)  { add_op(infix(opn, p), d, true); }
-    void add_infixl(name const & opn, unsigned p, name const & n) { add_op(infixl(opn, p), n, true); }
+    void add_infixl(name const & opn, unsigned p, expr const & d) { add_op(infixl(opn, p), d, true); }
-    void add_infixr(name const & opn, unsigned p, name const & n) { add_op(infixr(opn, p), n, true); }
+    void add_infixr(name const & opn, unsigned p, expr const & d) { add_op(infixr(opn, p), d, true); }
-    void add_prefix(name const & opn, unsigned p, name const & n) { add_op(prefix(opn, p), n, false); }
+    void add_prefix(name const & opn, unsigned p, expr const & d) { add_op(prefix(opn, p), d, false); }
-    void add_postfix(name const & opn, unsigned p, name const & n) { add_op(postfix(opn, p), n, true); }
+    void add_postfix(name const & opn, unsigned p, expr const & d) { add_op(postfix(opn, p), d, true); }
-    void add_mixfixl(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixl(sz, opns, p), n, false); }
+    void add_mixfixl(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixl(sz, opns, p), d, false); }
-    void add_mixfixr(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixr(sz, opns, p), n, true);  }
+    void add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixr(sz, opns, p), d, true);  }
-    void add_mixfixc(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixc(sz, opns, p), n, false); }
+    void add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixc(sz, opns, p), d, false); }
 
     imp(frontend & fe):
         m_num_children(0) {
@@ -211,15 +212,15 @@ frontend::object_iterator frontend::end_objects() const { return m_imp->m_env.en
 frontend::object_iterator frontend::begin_local_objects() const { return m_imp->m_env.begin_local_objects(); }
 frontend::object_iterator frontend::end_local_objects() const { return m_imp->m_env.end_local_objects(); }
 
-void frontend::add_infix(name const & opn, unsigned p, name const & n)  { m_imp->add_infix(opn, p, n); }
+void frontend::add_infix(name const & opn, unsigned p, expr const & d)  { m_imp->add_infix(opn, p, d); }
-void frontend::add_infixl(name const & opn, unsigned p, name const & n)  { m_imp->add_infixl(opn, p, n); }
+void frontend::add_infixl(name const & opn, unsigned p, expr const & d)  { m_imp->add_infixl(opn, p, d); }
-void frontend::add_infixr(name const & opn, unsigned p, name const & n)  { m_imp->add_infixr(opn, p, n); }
+void frontend::add_infixr(name const & opn, unsigned p, expr const & d)  { m_imp->add_infixr(opn, p, d); }
-void frontend::add_prefix(name const & opn, unsigned p, name const & n)  { m_imp->add_prefix(opn, p, n); }
+void frontend::add_prefix(name const & opn, unsigned p, expr const & d)  { m_imp->add_prefix(opn, p, d); }
-void frontend::add_postfix(name const & opn, unsigned p, name const & n) { m_imp->add_postfix(opn, p, n); }
+void frontend::add_postfix(name const & opn, unsigned p, expr const & d) { m_imp->add_postfix(opn, p, d); }
-void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixl(sz, opns, p, n); }
+void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixl(sz, opns, p, d); }
-void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixr(sz, opns, p, n); }
+void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixr(sz, opns, p, d); }
-void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixc(sz, opns, p, n); }
+void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixc(sz, opns, p, d); }
-operator_info frontend::find_op_for(name const & n) const { return m_imp->find_op_for(n); }
+operator_info frontend::find_op_for(expr const & n) const { return m_imp->find_op_for(n); }
 operator_info frontend::find_nud(name const & n) const { return m_imp->find_nud(n); }
 operator_info frontend::find_led(name const & n) const { return m_imp->find_led(n); }
 }

src/frontend/frontend.h

@@ -23,8 +23,10 @@ public:
     frontend();
     ~frontend();
 
-    // =======================================
+    /**
-    // Parent/Child frontend management
+       @name Parent/Child frontend management.
+    */
+    /*@{*/
     /**
         \brief Create a child environment. This frontend object will
         only allow "read-only" operations until all children frontend
@@ -40,14 +42,16 @@ public:
 
     /** \brief Return parent frontend */
     frontend parent() const;
-    // =======================================
+    /*@}*/
 
+    /**
+       @name Environment API
+    */
+    /*@{*/
     /** \brief Coercion frontend -> environment. */
     environment const & get_environment() const;
     operator environment const &() const { return get_environment(); }
 
-    // =======================================
-    // Environment API
     level add_uvar(name const & n, level const & l);
     level add_uvar(name const & n);
     level get_uvar(name const & n) const;
@@ -64,30 +68,50 @@ public:
     object_iterator end_objects() const;
     object_iterator begin_local_objects() const;
     object_iterator end_local_objects() const;
-    // =======================================
+    /*@}*/
 
-    // =======================================
-    // Notation
-    void add_infix(name const & opn, unsigned precedence, name const & n);
-    void add_infixl(name const & opn, unsigned precedence, name const & n);
-    void add_infixr(name const & opn, unsigned precedence, name const & n);
-    void add_prefix(name const & opn, unsigned precedence, name const & n);
-    void add_postfix(name const & opn, unsigned precedence, name const & n);
-    void add_mixfixl(unsigned sz, name const * opns, unsigned precedence, name const & n);
-    void add_mixfixr(unsigned sz, name const * opns, unsigned precedence, name const & n);
-    void add_mixfixc(unsigned sz, name const * opns, unsigned precedence, name const & n);
     /**
-        \brief Return the operator (if it exists) associated with the
+       @name Notation for parsing and pretty printing.
-        given internal name.
-
-        \remark If an operator is not associated with \c n, then
-        return the null operator.
     */
-    operator_info find_op_for(name const & n) const;
+    /*@{*/
+    void add_infix(name const & opn, unsigned precedence, expr const & d);
+    void add_infixl(name const & opn, unsigned precedence, expr const & d);
+    void add_infixr(name const & opn, unsigned precedence, expr const & d);
+    void add_prefix(name const & opn, unsigned precedence, expr const & d);
+    void add_postfix(name const & opn, unsigned precedence, expr const & d);
+    void add_mixfixl(unsigned sz, name const * opns, unsigned precedence, expr const & d);
+    void add_mixfixr(unsigned sz, name const * opns, unsigned precedence, expr const & d);
+    void add_mixfixc(unsigned sz, name const * opns, unsigned precedence, expr const & d);
+    /**
+        \brief Return the operator (if one exists) associated with the
+        given expression.
 
+        \remark If an operator is not associated with \c e, then
+        return the null operator.
+
+        \remark This is used for pretty printing.
+    */
+    operator_info find_op_for(expr const & e) const;
+    /**
+       \brief Return the operator (if one exists) that can appear at
+       the beginning of a language construct.
+
+        \remark If there isn't a nud operator starting with \c n, then
+        return the null operator.
+
+        \remark This is used for parsing.
+    */
     operator_info find_nud(name const & n) const;
+    /**
+       \brief Return the operator (if one exists) that can appear
+       inside of a language construct.
 
+        \remark If there isn't a led operator starting with \c n, then
+        return the null operator.
+
+        \remark This is used for parsing.
+    */
     operator_info find_led(name const & n) const;
-    // =======================================
+    /*@}*/
 };
 }

src/frontend/operator_info.cpp

@@ -16,7 +16,7 @@ struct operator_info::imp {
     fixity        m_fixity;
     unsigned      m_precedence;
     list<name>    m_op_parts;  // operator parts, > 1 only if the operator is mixfix.
-    list<name>    m_names;     // internal names, > 1 only if the operator is overloaded.
+    list<expr>    m_exprs;     // possible interpretations for the operator.
 
     imp(name const & op, fixity f, unsigned p):
         m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(cons(op, list<name>())) {}
@@ -27,7 +27,7 @@ struct operator_info::imp {
     }
 
     imp(imp const & s):
-        m_rc(1), m_fixity(s.m_fixity), m_precedence(s.m_precedence), m_op_parts(s.m_op_parts), m_names(s.m_names) {
+        m_rc(1), m_fixity(s.m_fixity), m_precedence(s.m_precedence), m_op_parts(s.m_op_parts), m_exprs(s.m_exprs) {
     }
 
     bool is_eq(imp const & other) const {
@@ -51,11 +51,11 @@ operator_info & operator_info::operator=(operator_info const & s) { LEAN_COPY_RE
 
 operator_info & operator_info::operator=(operator_info && s) { LEAN_MOVE_REF(operator_info, s); }
 
-void operator_info::add_internal_name(name const & n) { lean_assert(m_ptr); m_ptr->m_names = cons(n, m_ptr->m_names); }
+void operator_info::add_expr(expr const & d) { lean_assert(m_ptr); m_ptr->m_exprs = cons(d, m_ptr->m_exprs); }
 
-bool operator_info::is_overloaded() const { return m_ptr && !is_nil(m_ptr->m_names) && !is_nil(cdr(m_ptr->m_names)); }
+bool operator_info::is_overloaded() const { return m_ptr && !is_nil(m_ptr->m_exprs) && !is_nil(cdr(m_ptr->m_exprs)); }
 
-list<name> const & operator_info::get_internal_names() const { lean_assert(m_ptr); return m_ptr->m_names; }
+list<expr> const & operator_info::get_exprs() const { lean_assert(m_ptr); return m_ptr->m_exprs; }
 
 fixity operator_info::get_fixity() const { lean_assert(m_ptr); return m_ptr->m_fixity; }
 
@@ -134,13 +134,4 @@ std::ostream & operator<<(std::ostream & out, operator_info const & o) {
     out << pp(o);
     return out;
 }
-
-format pp(notation_declaration const & n) {
-    return format{pp(n.get_op()), space(), format(n.get_internal_name())};
-}
-
-std::ostream & operator<<(std::ostream & out, notation_declaration const & n) {
-    out << pp(n);
-    return out;
-}
 }

src/frontend/operator_info.h

@@ -28,7 +28,6 @@ enum class fixity { Prefix, Infix, Infixl, Infixr, Postfix, Mixfixl, Mixfixr, Mi
    \brief Data-structure for storing user defined operator
    information. This information is used during parsing and
    pretty-printing.
-
 */
 class operator_info {
     struct imp;
@@ -56,20 +55,19 @@ public:
     friend operator_info mixfixr(unsigned num_parts, name const * parts, unsigned precedence);
     friend operator_info mixfixc(unsigned num_parts, name const * parts, unsigned precedence);
 
-    /** \brief Associate an internal name for this operator. */
+    /** \brief Associate a denotation (expression) with this operator. */
-    void add_internal_name(name const & n);
+    void add_expr(expr const & n);
 
     /** \brief Return true iff the operator is overloaded. */
     bool is_overloaded() const;
 
     /**
-       \brief Return the list of internal names for this operator.
+       \brief Return the list of expressions for this operator.
        The list has size greater than 1 iff the operator has been
        overloaded.
-       Internal names are the real names used to identify the operator
+       These are the possible interpretations for the operator.
-       in the kernel.
     */
-    list<name> const & get_internal_names() const;
+    list<expr> const & get_exprs() const;
 
     /** \brief Return the operator fixity. */
     fixity get_fixity() const;
@@ -110,15 +108,12 @@ std::ostream & operator<<(std::ostream & out, operator_info const & o);
 */
 class notation_declaration : public neutral_object_cell {
     operator_info m_op;
-    name          m_name;
+    expr          m_expr;
 public:
-    notation_declaration(operator_info const & op, name const & n):m_op(op), m_name(n) {}
+    notation_declaration(operator_info const & op, expr const & n):m_op(op), m_expr(n) {}
     virtual ~notation_declaration() {}
     virtual char const * keyword() const;
     operator_info get_op() const { return m_op; }
-    name const & get_internal_name() const { return m_name; }
+    expr const & get_expr() const { return m_expr; }
 };
-
-format pp(notation_declaration const & n);
-std::ostream & operator<<(std::ostream & out, notation_declaration const & n);
 }

src/frontend/parser.cpp

@@ -288,13 +288,13 @@ class parser_fn {
        resolve/decide which f_i should be used.
     */
     expr mk_fun(operator_info const & op) {
-        list<name> const & fs = op.get_internal_names();
+        list<expr> const & fs = op.get_exprs();
         lean_assert(!is_nil(fs));
         auto it = fs.begin();
-        expr r = mk_constant(*it);
+        expr r = *it;
         ++it;
         for (; it != fs.end(); ++it)
-            r = mk_app(g_overload, mk_constant(*it), r);
+            r = mk_app(g_overload, *it, r);
         return r;
     }
 
@@ -870,19 +870,20 @@ class parser_fn {
         \brief Parse prefix/postfix/infix/infixl/infixr user operator
         definitions. These definitions have the form:
 
-           - fixity [Num] ID ID
+           - fixity [Num] ID ':' expr
     */
     void parse_op(fixity fx) {
         next();
         unsigned prec = parse_precedence();
         name op_id = parse_op_id();
-        name id    = parse_op_id();
+        check_colon_next("invalid operator definition, ':' expected");
+        expr d     = parse_expr();
         switch (fx) {
-        case fixity::Prefix:  m_frontend.add_prefix(op_id, prec, id); break;
+        case fixity::Prefix:  m_frontend.add_prefix(op_id, prec, d); break;
-        case fixity::Postfix: m_frontend.add_postfix(op_id, prec, id); break;
+        case fixity::Postfix: m_frontend.add_postfix(op_id, prec, d); break;
-        case fixity::Infix:   m_frontend.add_infix(op_id, prec, id); break;
+        case fixity::Infix:   m_frontend.add_infix(op_id, prec, d); break;
-        case fixity::Infixl:  m_frontend.add_infixl(op_id, prec, id); break;
+        case fixity::Infixl:  m_frontend.add_infixl(op_id, prec, d); break;
-        case fixity::Infixr:  m_frontend.add_infixr(op_id, prec, id); break;
+        case fixity::Infixr:  m_frontend.add_infixr(op_id, prec, d); break;
         default: lean_unreachable(); break;
         }
     }
@@ -891,7 +892,7 @@ class parser_fn {
         \brief Parse mixfix/mixfixl/mixfixr user operator definition.
         These definitions have the form:
 
-        - fixity [NUM] ID ID+ ID
+        - fixity [NUM] ID ID+ ':' ID
     */
     void parse_mixfix_op(fixity fx) {
         next();
@@ -899,16 +900,16 @@ class parser_fn {
         buffer<name> parts;
         parts.push_back(parse_op_id());
         parts.push_back(parse_op_id());
-        name id = parse_op_id();
+        while (!curr_is_colon()) {
-        while (curr_is_identifier()) {
+            parts.push_back(parse_op_id());
-            parts.push_back(id);
-            id = curr_name();
-            next();
         }
+        lean_assert(curr_is_colon());
+        next();
+        expr d = parse_expr();
         switch (fx) {
-        case fixity::Mixfixl:  m_frontend.add_mixfixl(parts.size(), parts.data(), prec, id); break;
+        case fixity::Mixfixl:  m_frontend.add_mixfixl(parts.size(), parts.data(), prec, d); break;
-        case fixity::Mixfixr:  m_frontend.add_mixfixr(parts.size(), parts.data(), prec, id); break;
+        case fixity::Mixfixr:  m_frontend.add_mixfixr(parts.size(), parts.data(), prec, d); break;
-        case fixity::Mixfixc:  m_frontend.add_mixfixc(parts.size(), parts.data(), prec, id); break;
+        case fixity::Mixfixc:  m_frontend.add_mixfixc(parts.size(), parts.data(), prec, d); break;
         default: lean_unreachable(); break;
         }
     }

src/frontend/pp.cpp

@@ -179,20 +179,21 @@ class pp_fn {
 
     /**
        \brief Return the operator associated with \c e.
-       Return the nil operator if there is none.
+       Return the null operator if there is none.
 
        We say \c e has an operator associated with it, if:
 
-       1) It is a constant and there is an operator associated with it.
+       1) \c e is associated with an operator.
 
-       2) It is an application, and the function is a constant \c c with an
+       2) It is an application, and the function is associated with an
-       operator associated with \c c.
+       operator.
     */
     operator_info get_operator(expr const & e) {
-        if (is_constant(e))
+        operator_info op = m_frontend.find_op_for(e);
-            return m_frontend.find_op_for(const_name(e));
+        if (op)
-        else if (is_app(e) && is_constant(arg(e, 0)))
+            return op;
-            return m_frontend.find_op_for(const_name(arg(e, 0)));
+        else if (is_app(e))
+            return m_frontend.find_op_for(arg(e, 0));
         else
             return operator_info();
     }
@@ -866,7 +867,8 @@ class pp_formatter_cell : public formatter_cell {
     }
 
     format pp_notation_decl(object const & obj) {
-        return ::lean::pp(*(static_cast<notation_declaration const *>(obj.cell())));
+        notation_declaration const & n = *(static_cast<notation_declaration const *>(obj.cell()));
+        return format{::lean::pp(n.get_op()), space(), colon(), space(), pp(n.get_expr())};
     }
 
 public:

src/tests/frontend/frontend.cpp

@@ -28,17 +28,17 @@ static void tst2() {
     operator_info op2 = infixr(name("implies"), 20);
     lean_assert(op1.get_precedence() == 10);
     lean_assert(op1.get_fixity() == fixity::Infixl);
-    op1.add_internal_name(name{"Bool","And"});
+    op1.add_expr(mk_and_fn());
     operator_info op3 = infixl(name("+"), 10);
-    op3.add_internal_name(name{"Int", "plus"});
+    op3.add_expr(Const(name{"Int", "plus"}));
-    op3.add_internal_name(name{"Real", "plus"});
+    op3.add_expr(Const(name{"Real", "plus"}));
-    std::cout << op3.get_internal_names() << "\n";
+    std::cout << op3.get_exprs() << "\n";
-    lean_assert(length(op3.get_internal_names()) == 2);
+    lean_assert(length(op3.get_exprs()) == 2);
     operator_info op4 = op3.copy();
-    op4.add_internal_name(name{"Complex", "plus"});
+    op4.add_expr(Const(name{"Complex", "plus"}));
-    std::cout << op4.get_internal_names() << "\n";
+    std::cout << op4.get_exprs() << "\n";
-    lean_assert(length(op3.get_internal_names()) == 2);
+    lean_assert(length(op3.get_exprs()) == 2);
-    lean_assert(length(op4.get_internal_names()) == 3);
+    lean_assert(length(op4.get_exprs()) == 3);
     lean_assert(op4.get_fixity() == fixity::Infixl);
     lean_assert(op4.get_op_name() == op3.get_op_name());
     lean_assert(prefix("tst", 20).get_fixity() == fixity::Prefix);
@@ -120,7 +120,7 @@ static void tst7() {
 static void tst8() {
     frontend fe;
     formatter fmt = mk_pp_formatter(fe);
-    fe.add_infixl("<-$->", 10, const_name(mk_refl_fn()));
+    fe.add_infixl("<-$->", 10, mk_refl_fn());
     std::cout << fmt(fe.find_object("Trivial")) << "\n";
 }
 
@@ -152,9 +152,9 @@ static void tst9() {
     bool found = false;
     std::for_each(f.begin_objects(), f.end_objects(), [&](object const & obj) { if (obj.has_name() && obj.get_name() == "y") found = true; });
     lean_assert(found);
-    f.add_postfix("!", 10, "factorial");
+    f.add_postfix("!", 10, Const("factorial"));
     name parts[] = {"if", "then", "else"};
-    f.add_mixfixl(3, parts, 10, "if");
+    f.add_mixfixl(3, parts, 10, Const("if"));
 }
 
 static void tst10() {

src/tests/frontend/parser.cpp

@@ -32,8 +32,8 @@ static void tst1() {
     parse(fe, "Variable x : Bool Variable y : Bool Axiom H : x && y || x => x");
     parse(fe, "Eval true && true");
     parse(fe, "Show true && false Eval true && false");
-    parse(fe, "Infixl 35 & and Show true & false & false Eval true & false");
+    parse(fe, "Infixl 35 & : and Show true & false & false Eval true & false");
-    parse(fe, "Mixfixc 100 if then fi implies Show if true then false fi");
+    parse(fe, "Mixfixc 100 if then fi : implies Show if true then false fi");
     parse(fe, "Show Pi (A : Type), A -> A");
     parse(fe, "Check Pi (A : Type), A -> A");
 }