refactor(kernel): remove heterogeneous equality

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

doc/lean/expr.md

@@ -57,49 +57,3 @@ definition inc (x : Nat) : Nat := x + 1
 eval inc (inc (inc 2))
 eval max (inc 2) 2 = 3
 ```
-
-## Heterogeneous equality
-
-For technical reasons, in Lean, we have heterogenous and homogeneous equality. In a nutshell, heterogenous is mainly used internally, and
-homogeneous are used externally when writing programs and specifications in Lean.
-Heterogenous equality allows us to compare elements of any type, and homogenous equality is just a definition on top of the heterogenous equality that expects arguments of the same type.
-The expression `t == s` is a heterogenous equality that is true iff `t` and `s` have the same interpretation.
-In the following example, we evaluate the expressions `1 == 2` and `2 == 2`. The first evaluates to `false` and the second to `true`.
-
-```lean
-eval 1 == 2
-eval 2 == 2
-```
-
-Since we can compare elements of different types, the following
-expression is type correct, but Lean normalizer/evaluator will *not*
-reduce it.
-
-```lean
-eval 2 == true
-```
-
-We strongly discourage users from directly using heterogeneous equality. The main problem is that it is very easy to
-write nonsensical expressions like the one above. The expression `t = s` is a homogeneous equality.
-It expects `t` and `s` to have the same type. Thus, the expression `2 = true` is type incorrect in Lean.
-The symbol `=` is just notation. Internally, homogeneous equality is defined as:
-
-```
-definition eq {A : (Type U)} (x y : A) : Bool := x == y
-infix 50 = : eq
-```
-
-The curly braces indicate that the first argument of `eq` is implicit. The symbol `=` is just a syntax sugar for `eq`.
-In the following example, we use the `set_option` command to force Lean to display implicit arguments and
-disable notation when pretty printing expressions.
-
-```lean
-set_option pp::implicit true
-set_option pp::notation false
-check 1 = 2
-
--- restore default configuration
-set_option pp::implicit false
-set_option pp::notation true
-check 1 = 2
-```

src/builtin/CMakeLists.txt

@@ -93,7 +93,7 @@ add_theory("if_then_else.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
 add_theory("Int.lean"          "${CMAKE_CURRENT_BINARY_DIR}/if_then_else.olean")
 add_theory("Real.lean"         "${CMAKE_CURRENT_BINARY_DIR}/Int.olean")
 add_theory("specialfn.lean"    "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
-add_theory("cast.lean"         "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
+## add_theory("cast.lean"         "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
 
 update_interface("kernel.olean"       "kernel" "-n")
 update_interface("Nat.olean"          "library/arith" "-n")

src/builtin/kernel.lean

@@ -1,34 +1,39 @@
 import macros
 
-universe U ≥ 1
+universe U   ≥ 1
+universe U' >= U + 1
 
 variable Bool : Type
 -- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions
 builtin true : Bool
 builtin false : Bool
 
-definition TypeU := (Type U)
+definition TypeU  := (Type U)
+definition TypeU' := (Type U')
+
+builtin eq {A : (Type U')} (a b : A) : Bool
+infix 50 = : eq
 
 definition not (a : Bool) := a → false
 
 notation 40 ¬ _ : not
 
 definition or (a b : Bool) := ¬ a → b
-
 infixr 30 || : or
 infixr 30 \/ : or
 infixr 30 ∨  : or
 
 definition and (a b : Bool) := ¬ (a → ¬ b)
-
 infixr 35 && : and
 infixr 35 /\ : and
 infixr 35 ∧  : and
 
+definition neq {A : TypeU} (a b : A) := ¬ (a = b)
+infix 50 ≠ : neq
+
 definition implies (a b : Bool) := a → b
 
-definition iff (a b : Bool) := a == b
+definition iff (a b : Bool) := a = b
-
 infixr 25 <-> : iff
 infixr 25 ↔   : iff
 
@@ -42,38 +47,30 @@ infixr 25 ↔   : iff
 -- want to treat exists as a constant.
 definition Exists (A : TypeU) (P : A → Bool) := ¬ (∀ x : A, ¬ (P x))
 
-definition eq {A : TypeU} (a b : A) := a == b
-
-infix 50 = : eq
-
-definition neq {A : TypeU} (a b : A) := ¬ (a = b)
-
-infix 50 ≠ : neq
-
 theorem em (a : Bool) : a ∨ ¬ a
 := assume Hna : ¬ a, Hna
 
 axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
 
-axiom refl {A : TypeU} (a : A) : a = a
+axiom refl {A : TypeU'} (a : A) : a = a
 
-axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b
+axiom subst {A : TypeU'} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b
 
 -- Function extensionality
-axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x == g x) : f == g
+axiom funext {A : TypeU'} {B : A → TypeU'} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g
 
 -- Forall extensionality
-axiom allext {A : TypeU} {B C : A → TypeU} (H : ∀ x : A, B x == C x) : (∀ x : A, B x) == (∀ x : A, C x)
+axiom allext {A : TypeU} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x : A, B x) = (∀ x : A, C x)
 
 -- Alias for subst where we can provide P explicitly, but keep A,a,b implicit
-theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b
+theorem substp {A : TypeU'} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b
 := subst H1 H2
 
 -- We will mark not as opaque later
 theorem not_intro {a : Bool} (H : a → false) : ¬ a
 := H
 
-theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
+theorem eta {A : TypeU'} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
 := funext (λ x : A, refl (f x))
 
 theorem trivial : true
@@ -157,10 +154,10 @@ theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
 theorem refute {a : Bool} (H : ¬ a → false) : a
 := or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1))
 
-theorem symm {A : TypeU} {a b : A} (H : a = b) : b = a
+theorem symm {A : TypeU'} {a b : A} (H : a = b) : b = a
 := subst (refl a) H
 
-theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
+theorem trans {A : TypeU'} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
 := subst H1 H2
 
 infixl 100 ⋈ : trans
@@ -174,39 +171,20 @@ theorem eq_ne_trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠
 theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c
 := subst H1 H2
 
-theorem heq_congr {A : TypeU} {a b c d : A} (H1 : a == c) (H2 : b == d) : (a == b) = (c == d)
-:= calc (a == b) = (c == b) : { H1 }
-             ... = (c == d) : { H2 }
-
-theorem heq_congrl {A : TypeU} {a : A} (b : A) {c : A} (H : a == c) : (a == b) = (c == b)
-:= heq_congr H (refl b)
-
-theorem heq_congrr {A : TypeU} (a : A) {b d : A} (H : b == d) : (a == b) = (a == d)
-:= heq_congr (refl a) H
-
 theorem eqt_elim {a : Bool} (H : a = true) : a
 := (symm H) ◂ trivial
 
 theorem eqf_elim {a : Bool} (H : a = false) : ¬ a
 := not_intro (λ Ha : a, H ◂ Ha)
 
-theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a
+theorem congr1 {A : TypeU'} {B : A → TypeU'} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a
 := substp (fun h : (∀ x : A, B x), f a = h a) (refl (f a)) H
 
--- We must use heterogenous equality in this theorem because (f a) : (B a) and (f b) : (B b)
+theorem congr2 {A B : TypeU'} {a b : A} (f : A → B) (H : a = b) : f a = f b
-theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : ∀ x : A, B x) (H : a = b) : f a == f b
-:= substp (fun x : A, f a == f x) (refl (f a)) H
-
-theorem congr {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} {a b : A} (H1 : f = g) (H2 : a = b) : f a == g b
-:= subst (congr2 f H2) (congr1 b H1)
-
--- Simpler version of congr2 theorem for arrows (i.e., non-dependent types)
-theorem scongr2 {A B : TypeU} {a b : A} (f : A → B) (H : a = b) : f a = f b
 := substp (fun x : A, f a = f x) (refl (f a)) H
 
--- Simpler version of congr theorem for arrows (i.e., non-dependent types)
+theorem congr {A B : TypeU'} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
-theorem scongr {A B : TypeU} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
+:= subst (congr2 f H2) (congr1 b H1)
-:= subst (scongr2 f H2) (congr1 b H1)
 
 -- Recall that exists is defined as ¬ ∀ x : A, ¬ P x
 theorem exists_elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B
@@ -241,7 +219,7 @@ theorem eqf_intro {a : Bool} (H : ¬ a) : a = false
 theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : a = b ↔ false
 := eqf_intro H
 
-theorem or_comm (a b : Bool) : a ∨ b ↔ b ∨ a
+theorem or_comm (a b : Bool) : (a ∨ b) = (b ∨ a)
 := boolext (assume H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a))
            (assume H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b))
 
@@ -490,7 +468,7 @@ theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H
 theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ↔ c ∧ d
 := and_congrr (λ H, H_ac) H_bd
 
-theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) ↔ p ∨ ∀ x, φ x
+theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x)
 := boolext
      (assume H : (∀ x, p ∨ φ x),
         or_elim (em p)
@@ -503,10 +481,10 @@ theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x,
               (λ H1 : p,          or_introl H1 (φ x))
               (λ H2 : (∀ x, φ x), or_intror p  (H2 x)))
 
-theorem forall_or_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) ↔ (∀ x, φ x) ∨ p
+theorem forall_or_distributel {A : Type} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) = ((∀ x, φ x) ∨ p)
 := calc (∀ x, φ x ∨ p) = (∀ x, p ∨ φ x)   : allext (λ x, or_comm (φ x) p)
-                  ...  = (p ∨ ∀ x, φ x)   : forall_or_distributer p φ
+                   ...  = (p ∨ ∀ x, φ x)   : forall_or_distributer p φ
-                  ...  = ((∀ x, φ x) ∨ p) : or_comm p (∀ x, φ x)
+                   ...  = ((∀ x, φ x) ∨ p) : or_comm p (∀ x, φ x)
 
 theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ↔ (∀ x, φ x) ∧ (∀ x, ψ x)
 := boolext

src/builtin/name_conv.lua

@@ -1,4 +1,8 @@
 -- Output a C++ statement that creates the given name
+function sanitize(s)
+   s, _ = string.gsub(s, "'", "_")
+   return s
+end
 function name_to_cpp_expr(n)
    function rec(n)
       if not n:is_atomic() then
@@ -6,7 +10,8 @@ function name_to_cpp_expr(n)
          io.write(", ")
       end
       if n:is_string() then
-         io.write("\"" .. n:get_string() .. "\"")
+         local s = n:get_string()
+         io.write("\"" .. sanitize(s) .. "\"")
       else
          error("numeral hierarchical names are not supported in the C++ interface: " .. tostring(n))
       end
@@ -31,7 +36,8 @@ function name_to_cpp_decl(n)
       io.write("_")
    end
    if n:is_string() then
-      io.write(n:get_string())
+      local s = n:get_string()
+      io.write(sanitize(s))
    else
       error("numeral hierarchical names are not supported in the C++ interface: " .. tostring(n))
    end

src/frontends/lean/notation.h

@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #pragma once
 #include <limits>
 namespace lean {
-constexpr unsigned g_eq_precedence    = 50;
 constexpr unsigned g_arrow_precedence = 25;
 constexpr unsigned g_app_precedence   = std::numeric_limits<unsigned>::max();
 }

src/frontends/lean/parser_calc.cpp

@@ -44,10 +44,18 @@ void calc_proof_parser::add_trans_step(expr const & op1, expr const & op2, trans
     m_trans_ops.emplace_front(op1, op2, d);
 }
 
+static expr get_value_op(expr const & op) {
+    if (is_value(op))
+        return mk_constant(to_value(op).get_name());
+    else
+        return op;
+}
+
+
 calc_proof_parser::calc_proof_parser() {
-    expr imp = mk_implies_fn();
+    expr imp = get_value_op(mk_implies_fn());
-    expr eq  = mk_eq_fn();
+    expr eq  = get_value_op(mk_eq_fn());
-    expr neq = mk_neq_fn();
+    expr neq = get_value_op(mk_neq_fn());
 
     add_supported_operator(op_data(imp, 2));
     add_supported_operator(op_data(eq, 3));

src/frontends/lean/parser_expr.cpp

@@ -563,14 +563,6 @@ expr parser_imp::parse_led_id(expr const & left) {
     }
 }
 
-/** \brief Parse <tt>expr '=' expr</tt>. */
-expr parser_imp::parse_heq(expr const & left) {
-    auto p = pos();
-    next();
-    expr right = parse_expr(g_eq_precedence);
-    return save(mk_heq(left, right), p);
-}
-
 /** \brief Parse <tt>expr '->' expr</tt>. */
 expr parser_imp::parse_arrow(expr const & left) {
     auto p = pos();
@@ -949,7 +941,6 @@ expr parser_imp::mk_app_left(expr const & left, expr const & arg) {
 expr parser_imp::parse_led(expr const & left) {
     switch (curr()) {
     case scanner::token::Id:          return parse_led_id(left);
-    case scanner::token::Eq:          return parse_heq(left);
     case scanner::token::Arrow:       return parse_arrow(left);
     case scanner::token::LeftParen:   return mk_app_left(left, parse_lparen());
     case scanner::token::IntVal:      return mk_app_left(left, parse_nat_int());
@@ -979,7 +970,6 @@ unsigned parser_imp::curr_lbp() {
                 return g_app_precedence;
         }
     }
-    case scanner::token::Eq : return g_eq_precedence;
     case scanner::token::Arrow : return g_arrow_precedence;
     case scanner::token::LeftParen: case scanner::token::IntVal: case scanner::token::DecimalVal:
     case scanner::token::StringVal: case scanner::token::Type: case scanner::token::Placeholder:

src/frontends/lean/parser_imp.h

@@ -291,7 +291,6 @@ private:
                              pos_info const & p);
     expr parse_expr_macro(name const & id, pos_info const & p);
     expr parse_led_id(expr const & left);
-    expr parse_heq(expr const & left);
     expr parse_arrow(expr const & left);
     expr parse_lparen();
     void parse_names(buffer<std::pair<pos_info, name>> & result);

src/frontends/lean/pp.cpp

@@ -64,7 +64,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 static format g_Type_fmt      = highlight_builtin(format("Type"));
-static format g_eq_fmt        = format("==");
 static format g_lambda_n_fmt  = highlight_keyword(format("\u03BB"));
 static format g_Pi_n_fmt      = highlight_keyword(format("\u2200"));
 static format g_lambda_fmt    = highlight_keyword(format("fun"));
@@ -234,7 +233,7 @@ class pp_fn {
                 return is_atomic(arg(e, 1));
             else
                 return false;
-        case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::HEq: case expr_kind::Let:
+        case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
             return false;
         }
         return false;
@@ -441,8 +440,6 @@ class pp_fn {
         operator_info op = get_operator(e);
         if (op) {
             return op.get_precedence();
-        } else if (is_heq(e)) {
-            return g_eq_precedence;
         } else if (is_arrow(e)) {
             return g_arrow_precedence;
         } else if (is_lambda(e) || is_pi(e) || is_let(e) || is_exists(e)) {
@@ -459,8 +456,6 @@ class pp_fn {
         operator_info op = get_operator(e);
         if (op) {
             return op.get_fixity() == fx;
-        } else if (is_heq(e)) {
-            return fixity::Infix == fx;
         } else if (is_arrow(e)) {
             return fixity::Infixr == fx;
         } else {
@@ -1021,28 +1016,6 @@ class pp_fn {
         return mk_pair(group(r_format), r_weight);
     }
 
-    /** \brief Pretty print the child of an equality. */
-    result pp_heq_child(expr const & e, unsigned depth) {
-        if (is_atomic(e)) {
-            return pp(e, depth + 1);
-        } else {
-            if (g_eq_precedence < get_operator_precedence(e))
-                return pp(e, depth + 1);
-            else
-                return pp_child_with_paren(e, depth);
-        }
-    }
-
-    /** \brief Pretty print an equality */
-    result pp_heq(expr const & e, unsigned depth) {
-        result p_arg1, p_arg2;
-        format r_format;
-        p_arg1 = pp_heq_child(heq_lhs(e), depth);
-        p_arg2 = pp_heq_child(heq_rhs(e), depth);
-        r_format = group(format{p_arg1.first, space(), g_eq_fmt, line(), p_arg2.first});
-        return mk_result(r_format, p_arg1.second + p_arg2.second + 1);
-    }
-
     result pp_choice(expr const & e, unsigned depth) {
         lean_assert(is_choice(e));
         unsigned num = get_num_choices(e);
@@ -1121,7 +1094,6 @@ class pp_fn {
                 case expr_kind::Lambda:
                 case expr_kind::Pi:         r = pp_abstraction(e, depth); break;
                 case expr_kind::Type:       r = pp_type(e);               break;
-                case expr_kind::HEq:        r = pp_heq(e, depth);         break;
                 case expr_kind::Let:        r = pp_let(e, depth);         break;
                 case expr_kind::MetaVar:    r = pp_metavar(e, depth);     break;
                 }

src/frontends/lean/scanner.cpp

@@ -22,7 +22,6 @@ static name g_pi_name("forall");
 static name g_let_name("let");
 static name g_in_name("in");
 static name g_arrow_name("->");
-static name g_eq_name("==");
 static name g_exists_name("exists");
 static name g_Exists_name("Exists");
 static name g_exists_unicode("\u2203");
@@ -237,8 +236,6 @@ scanner::token scanner::read_b_symbol(char prev) {
             m_name_val = name(m_buffer.c_str());
             if (m_name_val == g_arrow_name)
                 return token::Arrow;
-            else if (m_name_val == g_eq_name)
-                return token::Eq;
             else
                 return token::Id;
         }

src/kernel/expr.cpp

@@ -141,17 +141,6 @@ expr mk_app(unsigned n, expr const * as) {
     to_app(r)->m_hash = hash_args(new_n, m_args);
     return r;
 }
-expr_heq::expr_heq(expr const & lhs, expr const & rhs):
-    expr_cell(expr_kind::HEq, ::lean::hash(lhs.hash(), rhs.hash()), lhs.has_metavar() || rhs.has_metavar()),
-    m_lhs(lhs),
-    m_rhs(rhs) {
-}
-expr_heq::~expr_heq() {}
-void expr_heq::dealloc(buffer<expr_cell*> & todelete) {
-    dec_ref(m_rhs, todelete);
-    dec_ref(m_lhs, todelete);
-    delete(this);
-}
 expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & b):
     expr_cell(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar()),
     m_name(n),
@@ -245,7 +234,6 @@ void expr_cell::dealloc() {
             case expr_kind::MetaVar:    delete static_cast<expr_metavar*>(it); break;
             case expr_kind::Type:       delete static_cast<expr_type*>(it); break;
             case expr_kind::Constant:   static_cast<expr_const*>(it)->dealloc(todo); break;
-            case expr_kind::HEq:        static_cast<expr_heq*>(it)->dealloc(todo); break;
             case expr_kind::App:        static_cast<expr_app*>(it)->dealloc(todo); break;
             case expr_kind::Lambda:     static_cast<expr_lambda*>(it)->dealloc(todo); break;
             case expr_kind::Pi:         static_cast<expr_pi*>(it)->dealloc(todo); break;
@@ -285,7 +273,6 @@ expr copy(expr const & a) {
     case expr_kind::Type:     return mk_type(ty_level(a));
     case expr_kind::Value:    return mk_value(static_cast<expr_value*>(a.raw())->m_val);
     case expr_kind::App:      return mk_app(num_args(a), begin_args(a));
-    case expr_kind::HEq:      return mk_heq(heq_lhs(a), heq_rhs(a));
     case expr_kind::Lambda:   return mk_lambda(abst_name(a), abst_domain(a), abst_body(a));
     case expr_kind::Pi:       return mk_pi(abst_name(a), abst_domain(a), abst_body(a));
     case expr_kind::Let:      return mk_let(let_name(a), let_type(a), let_value(a), let_body(a));
@@ -330,7 +317,7 @@ constexpr char g_first_app_size_kind = 32;
 constexpr char g_small_app_num_args  = 32;
 constexpr bool is_small(expr_kind k) { return 0 <= static_cast<char>(k) && static_cast<char>(k) < g_first_app_size_kind; }
 static_assert(is_small(expr_kind::Var) && is_small(expr_kind::Constant) && is_small(expr_kind::Value) && is_small(expr_kind::App) &&
-              is_small(expr_kind::Lambda) && is_small(expr_kind::Pi) && is_small(expr_kind::Type) && is_small(expr_kind::HEq) &&
+              is_small(expr_kind::Lambda) && is_small(expr_kind::Pi) && is_small(expr_kind::Type) &&
               is_small(expr_kind::Let) && is_small(expr_kind::MetaVar), "expr_kind is too big");
 
 class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp> {
@@ -373,7 +360,6 @@ class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp
                     for (unsigned i = 0; i < num_args(a); i++)
                         write_core(arg(a, i));
                     break;
-                case expr_kind::HEq:       write_core(heq_lhs(a)); write_core(heq_rhs(a)); break;
                 case expr_kind::Lambda:
                 case expr_kind::Pi:        s << abst_name(a); write_core(abst_domain(a)); write_core(abst_body(a)); break;
                 case expr_kind::Let:       s << let_name(a); write_core(let_type(a)); write_core(let_value(a)); write_core(let_body(a)); break;
@@ -430,10 +416,6 @@ public:
                         args.push_back(read());
                     return mk_app(args);
                 }
-                case expr_kind::HEq: {
-                    expr lhs = read();
-                    return mk_heq(lhs, read());
-                }
                 case expr_kind::Lambda: {
                     name n = read_name(d);
                     expr d = read();

src/kernel/expr.h

@@ -34,7 +34,6 @@ class value;
           |   Lambda        name expr expr
           |   Pi            name expr expr
           |   Type          universe
-          |   Eq            expr expr         (heterogeneous equality)
           |   Let           name expr expr expr
           |   Metavar       name local_context
 
@@ -52,7 +51,7 @@ The main API is divided in the following sections
 - Miscellaneous
 ======================================= */
 class expr;
-enum class expr_kind { Var, Constant, Value, App, Lambda, Pi, Type, HEq, Let, MetaVar };
+enum class expr_kind { Var, Constant, Value, App, Lambda, Pi, Type, Let, MetaVar };
 class local_entry;
 /**
    \brief A metavariable local context is just a list of local_entries.
@@ -142,7 +141,6 @@ public:
     friend expr mk_constant(name const & n, optional<expr> const & t);
     friend expr mk_value(value & v);
     friend expr mk_app(unsigned num_args, expr const * args);
-    friend expr mk_heq(expr const & l, expr const & r);
     friend expr mk_lambda(name const & n, expr const & t, expr const & e);
     friend expr mk_pi(name const & n, expr const & t, expr const & e);
     friend expr mk_type(level const & l);
@@ -213,18 +211,6 @@ public:
     expr const * begin_args() const          { return m_args; }
     expr const * end_args() const            { return m_args + m_num_args; }
 };
-/** \brief Heterogeneous equality */
-class expr_heq : public expr_cell {
-    expr m_lhs;
-    expr m_rhs;
-    friend class expr_cell;
-    void dealloc(buffer<expr_cell*> & todelete);
-public:
-    expr_heq(expr const & lhs, expr const & rhs);
-    ~expr_heq();
-    expr const & get_lhs() const { return m_lhs; }
-    expr const & get_rhs() const { return m_rhs; }
-};
 /** \brief Super class for lambda abstraction and pi (functional spaces). */
 class expr_abstraction : public expr_cell {
     name     m_name;
@@ -391,7 +377,6 @@ inline bool is_var(expr_cell * e)         { return e->kind() == expr_kind::Var;
 inline bool is_constant(expr_cell * e)    { return e->kind() == expr_kind::Constant; }
 inline bool is_value(expr_cell * e)       { return e->kind() == expr_kind::Value; }
 inline bool is_app(expr_cell * e)         { return e->kind() == expr_kind::App; }
-inline bool is_heq(expr_cell * e)         { return e->kind() == expr_kind::HEq; }
 inline bool is_lambda(expr_cell * e)      { return e->kind() == expr_kind::Lambda; }
 inline bool is_pi(expr_cell * e)          { return e->kind() == expr_kind::Pi; }
 inline bool is_type(expr_cell * e)        { return e->kind() == expr_kind::Type; }
@@ -403,7 +388,6 @@ inline bool is_var(expr const & e)         { return e.kind() == expr_kind::Var;
 inline bool is_constant(expr const & e)    { return e.kind() == expr_kind::Constant; }
 inline bool is_value(expr const & e)       { return e.kind() == expr_kind::Value; }
 inline bool is_app(expr const & e)         { return e.kind() == expr_kind::App; }
-inline bool is_heq(expr const & e)         { return e.kind() == expr_kind::HEq; }
 inline bool is_lambda(expr const & e)      { return e.kind() == expr_kind::Lambda; }
 inline bool is_pi(expr const & e)          { return e.kind() == expr_kind::Pi; }
        bool is_arrow(expr const & e);
@@ -430,8 +414,6 @@ inline expr mk_app(expr const & e1, expr const & e2) { return mk_app({e1, e2});
 inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { return mk_app({e1, e2, e3}); }
 inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({e1, e2, e3, e4}); }
 inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({e1, e2, e3, e4, e5}); }
-inline expr mk_heq(expr const & l, expr const & r) { return expr(new expr_heq(l, r)); }
-inline expr HEq(expr const & l, expr const & r) { return mk_heq(l, r); }
 inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); }
 inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
 inline bool is_default_arrow_var_name(name const & n) { return n == "a"; }
@@ -463,7 +445,6 @@ inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3,
 inline expr_var *         to_var(expr_cell * e)         { lean_assert(is_var(e));         return static_cast<expr_var*>(e); }
 inline expr_const *       to_constant(expr_cell * e)    { lean_assert(is_constant(e));    return static_cast<expr_const*>(e); }
 inline expr_app *         to_app(expr_cell * e)         { lean_assert(is_app(e));         return static_cast<expr_app*>(e); }
-inline expr_heq *         to_heq(expr_cell * e)         { lean_assert(is_heq(e));         return static_cast<expr_heq*>(e); }
 inline expr_abstraction * to_abstraction(expr_cell * e) { lean_assert(is_abstraction(e)); return static_cast<expr_abstraction*>(e); }
 inline expr_lambda *      to_lambda(expr_cell * e)      { lean_assert(is_lambda(e));      return static_cast<expr_lambda*>(e); }
 inline expr_pi *          to_pi(expr_cell * e)          { lean_assert(is_pi(e));          return static_cast<expr_pi*>(e); }
@@ -474,7 +455,6 @@ inline expr_metavar *     to_metavar(expr_cell * e)     { lean_assert(is_metavar
 inline expr_var *         to_var(expr const & e)         { return to_var(e.raw()); }
 inline expr_const *       to_constant(expr const & e)    { return to_constant(e.raw()); }
 inline expr_app *         to_app(expr const & e)         { return to_app(e.raw()); }
-inline expr_heq *         to_heq(expr const & e)         { return to_heq(e.raw()); }
 inline expr_abstraction * to_abstraction(expr const & e) { return to_abstraction(e.raw()); }
 inline expr_lambda *      to_lambda(expr const & e)      { return to_lambda(e.raw()); }
 inline expr_pi *          to_pi(expr const & e)          { return to_pi(e.raw()); }
@@ -496,8 +476,6 @@ inline optional<expr> const &  const_type(expr_cell * e) { return to_constant(e)
 inline value const & to_value(expr_cell * e)             { lean_assert(is_value(e)); return static_cast<expr_value*>(e)->get_value(); }
 inline unsigned      num_args(expr_cell * e)             { return to_app(e)->get_num_args(); }
 inline expr const &  arg(expr_cell * e, unsigned idx)    { return to_app(e)->get_arg(idx); }
-inline expr const &  heq_lhs(expr_cell * e)              { return to_heq(e)->get_lhs(); }
-inline expr const &  heq_rhs(expr_cell * e)              { return to_heq(e)->get_rhs(); }
 inline name const &  abst_name(expr_cell * e)            { return to_abstraction(e)->get_name(); }
 inline expr const &  abst_domain(expr_cell * e)          { return to_abstraction(e)->get_domain(); }
 inline expr const &  abst_body(expr_cell * e)            { return to_abstraction(e)->get_body(); }
@@ -529,8 +507,6 @@ inline unsigned      num_args(expr const & e)             { return to_app(e)->ge
 inline expr const &  arg(expr const & e, unsigned idx)    { return to_app(e)->get_arg(idx); }
 inline expr const *  begin_args(expr const & e)           { return to_app(e)->begin_args(); }
 inline expr const *  end_args(expr const & e)             { return to_app(e)->end_args(); }
-inline expr const &  heq_lhs(expr const & e)              { return to_heq(e)->get_lhs(); }
-inline expr const &  heq_rhs(expr const & e)              { return to_heq(e)->get_rhs(); }
 inline name const &  abst_name(expr const & e)            { return to_abstraction(e)->get_name(); }
 inline expr const &  abst_domain(expr const & e)          { return to_abstraction(e)->get_domain(); }
 inline expr const &  abst_body(expr const & e)            { return to_abstraction(e)->get_body(); }
@@ -650,18 +626,6 @@ template<typename F> expr update_let(expr const & e, F f) {
     else
         return e;
 }
-template<typename F> expr update_heq(expr const & e, F f) {
-    static_assert(std::is_same<typename std::result_of<F(expr const &, expr const &)>::type,
-                  std::pair<expr, expr>>::value,
-                  "update_heq: return type of f is not pair<expr, expr>");
-    expr const & old_l = heq_lhs(e);
-    expr const & old_r = heq_rhs(e);
-    std::pair<expr, expr> p = f(old_l, old_r);
-    if (!is_eqp(p.first, old_l) || !is_eqp(p.second, old_r))
-        return mk_heq(p.first, p.second);
-    else
-        return e;
-}
 template<typename F> expr update_metavar(expr const & e, name const & n, F f) {
     static_assert(std::is_same<typename std::result_of<F(local_entry const &)>::type, local_entry>::value,
                   "update_metavar: return type of f(local_entry) is not local_entry");

src/kernel/expr_eq.h

@@ -64,7 +64,6 @@ class expr_eq_fn {
                 if (!apply(arg(a, i), arg(b, i)))
                     return false;
             return true;
-        case expr_kind::HEq:      return apply(heq_lhs(a), heq_lhs(b)) && apply(heq_rhs(a), heq_rhs(b));
         case expr_kind::Lambda:   // Remark: we ignore get_abs_name because we want alpha-equivalence
         case expr_kind::Pi:       return apply(abst_domain(a), abst_domain(b)) && apply(abst_body(a), abst_body(b));
         case expr_kind::Type:     return ty_level(a) == ty_level(b);

src/kernel/for_each_fn.h

@@ -85,10 +85,6 @@ class for_each_fn {
                 }
                 goto begin_loop;
             }
-            case expr_kind::HEq:
-                todo.emplace_back(heq_rhs(e), offset);
-                todo.emplace_back(heq_lhs(e), offset);
-                goto begin_loop;
             case expr_kind::Lambda:
             case expr_kind::Pi:
                 todo.emplace_back(abst_body(e), offset + 1);

src/kernel/free_vars.cpp

@@ -40,7 +40,7 @@ protected:
             return true;
         case expr_kind::Var:
             return var_idx(e) >= offset;
-        case expr_kind::App: case expr_kind::HEq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
+        case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
             break;
         }
 
@@ -78,9 +78,6 @@ protected:
         case expr_kind::App:
             result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); });
             break;
-        case expr_kind::HEq:
-            result = apply(heq_lhs(e), offset) || apply(heq_rhs(e), offset);
-            break;
         case expr_kind::Lambda:
         case expr_kind::Pi:
             result = apply(abst_domain(e), offset) || apply(abst_body(e), offset + 1);
@@ -170,7 +167,7 @@ class free_var_range_fn {
             return 0;
         case expr_kind::Var:
             return var_idx(e) + 1;
-        case expr_kind::MetaVar: case expr_kind::App: case expr_kind::HEq:
+        case expr_kind::MetaVar: case expr_kind::App:
         case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
             break;
         }
@@ -203,9 +200,6 @@ class free_var_range_fn {
             for (auto const & c : args(e))
                 result = std::max(result, apply(c));
             break;
-        case expr_kind::HEq:
-            result = std::max(apply(heq_lhs(e)), apply(heq_rhs(e)));
-            break;
         case expr_kind::Lambda:
         case expr_kind::Pi:
             result = std::max(apply(abst_domain(e)), dec(apply(abst_body(e))));
@@ -287,7 +281,7 @@ protected:
                 return true; // assume that any free variable can occur in the metavariable
         case expr_kind::Var:
             return in_interval(var_idx(e), offset);
-        case expr_kind::App: case expr_kind::HEq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
+        case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
             break;
         }
 
@@ -326,9 +320,6 @@ protected:
         case expr_kind::App:
             result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); });
             break;
-        case expr_kind::HEq:
-            result = apply(heq_lhs(e), offset) || apply(heq_rhs(e), offset);
-            break;
         case expr_kind::Lambda:
         case expr_kind::Pi:
             result = apply(abst_domain(e), offset) || apply(abst_body(e), offset + 1);

src/kernel/kernel.cpp

@@ -16,6 +16,8 @@ namespace lean {
 // Bultin universe variables m and u
 static level u_lvl(name("U"));
 expr const TypeU = Type(u_lvl);
+static level up_lvl(name("U'"));
+expr const TypeUp = Type(up_lvl);
 // =======================================
 
 // =======================================
@@ -78,6 +80,42 @@ bool is_false(expr const & e) {
 }
 // =======================================
 
+// =======================================
+// Equality
+static name   g_eq_name("eq");
+static format g_eq_fmt(g_eq_name);
+/**
+   \brief Semantic attachment for if-then-else operator with type
+   <code>Pi (A : Type), Bool -> A -> A -> A</code>
+*/
+class eq_fn_value : public value {
+    expr m_type;
+    static expr mk_type() {
+        expr A    = Const("A");
+        // Pi (A: TypeUp), A -> A -> Bool
+        return Pi({A, TypeUp}, (A >> (A >> Bool)));
+    }
+public:
+    eq_fn_value():m_type(mk_type()) {}
+    virtual ~eq_fn_value() {}
+    virtual expr get_type() const { return m_type; }
+    virtual name get_name() const { return g_eq_name; }
+    virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
+        if (num_args == 4 && is_value(args[2]) && is_value(args[3]) && typeid(to_value(args[2])) == typeid(to_value(args[3]))) {
+            return some_expr(mk_bool_value(args[2] == args[3]));
+        } else {
+            return none_expr();
+        }
+    }
+    virtual void write(serializer & s) const { s << "eq"; }
+};
+MK_BUILTIN(eq_fn, eq_fn_value);
+MK_IS_BUILTIN(is_eq_fn, mk_eq_fn());
+static register_builtin_fn eq_blt("eq", []() { return mk_eq_fn(); });
+static value::register_deserializer_fn eq_ds("eq", [](deserializer & ) { return mk_eq_fn(); });
+// =======================================
+
+
 void import_kernel(environment const & env, io_state const & ios) {
     env->import("kernel", ios);
 }

src/kernel/kernel.h

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 namespace lean {
 // See src/builtin/kernel.lean for signatures.
 extern expr const TypeU;
+extern expr const TypeUp;
 
 /** \brief Return the Lean Boolean type. */
 expr mk_bool_type();
@@ -33,6 +34,11 @@ bool is_true(expr const & e);
 /** \brief Return true iff \c e is the Lean false value. */
 bool is_false(expr const & e);
 
+expr mk_eq_fn();
+bool is_eq_fn(expr const & e);
+inline expr mk_eq(expr const & A, expr const & lhs, expr const & rhs) { return mk_app(mk_eq_fn(), A, lhs, rhs); }
+inline bool is_eq(expr const & e) { return is_app(e) && is_eq_fn(arg(e, 0)); }
+
 inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); }
 inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); }
 inline expr Or(expr const & e1, expr const & e2) { return mk_or(e1, e2); }

src/kernel/kernel_decls.cpp

@@ -8,14 +8,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 namespace lean {
 MK_CONSTANT(Bool, name("Bool"));
 MK_CONSTANT(TypeU, name("TypeU"));
+MK_CONSTANT(TypeU_, name("TypeU_"));
 MK_CONSTANT(not_fn, name("not"));
 MK_CONSTANT(or_fn, name("or"));
 MK_CONSTANT(and_fn, name("and"));
+MK_CONSTANT(neq_fn, name("neq"));
 MK_CONSTANT(implies_fn, name("implies"));
 MK_CONSTANT(iff_fn, name("iff"));
 MK_CONSTANT(exists_fn, name("exists"));
-MK_CONSTANT(eq_fn, name("eq"));
-MK_CONSTANT(neq_fn, name("neq"));
 MK_CONSTANT(em_fn, name("em"));
 MK_CONSTANT(case_fn, name("case"));
 MK_CONSTANT(refl_fn, name("refl"));
@@ -53,16 +53,11 @@ MK_CONSTANT(trans_fn, name("trans"));
 MK_CONSTANT(ne_symm_fn, name("ne_symm"));
 MK_CONSTANT(eq_ne_trans_fn, name("eq_ne_trans"));
 MK_CONSTANT(ne_eq_trans_fn, name("ne_eq_trans"));
-MK_CONSTANT(heq_congr_fn, name("heq_congr"));
-MK_CONSTANT(heq_congrl_fn, name("heq_congrl"));
-MK_CONSTANT(heq_congrr_fn, name("heq_congrr"));
 MK_CONSTANT(eqt_elim_fn, name("eqt_elim"));
 MK_CONSTANT(eqf_elim_fn, name("eqf_elim"));
 MK_CONSTANT(congr1_fn, name("congr1"));
 MK_CONSTANT(congr2_fn, name("congr2"));
 MK_CONSTANT(congr_fn, name("congr"));
-MK_CONSTANT(scongr2_fn, name("scongr2"));
-MK_CONSTANT(scongr_fn, name("scongr"));
 MK_CONSTANT(exists_elim_fn, name("exists_elim"));
 MK_CONSTANT(exists_intro_fn, name("exists_intro"));
 MK_CONSTANT(boolext_fn, name("boolext"));

src/kernel/kernel_decls.h

@@ -9,6 +9,8 @@ expr mk_Bool();
 bool is_Bool(expr const & e);
 expr mk_TypeU();
 bool is_TypeU(expr const & e);
+expr mk_TypeU_();
+bool is_TypeU_(expr const & e);
 expr mk_not_fn();
 bool is_not_fn(expr const & e);
 inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)); }
@@ -21,6 +23,10 @@ expr mk_and_fn();
 bool is_and_fn(expr const & e);
 inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)); }
 inline expr mk_and(expr const & e1, expr const & e2) { return mk_app({mk_and_fn(), e1, e2}); }
+expr mk_neq_fn();
+bool is_neq_fn(expr const & e);
+inline bool is_neq(expr const & e) { return is_app(e) && is_neq_fn(arg(e, 0)); }
+inline expr mk_neq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_fn(), e1, e2, e3}); }
 expr mk_implies_fn();
 bool is_implies_fn(expr const & e);
 inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); }
@@ -33,14 +39,6 @@ expr mk_exists_fn();
 bool is_exists_fn(expr const & e);
 inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)); }
 inline expr mk_exists(expr const & e1, expr const & e2) { return mk_app({mk_exists_fn(), e1, e2}); }
-expr mk_eq_fn();
-bool is_eq_fn(expr const & e);
-inline bool is_eq(expr const & e) { return is_app(e) && is_eq_fn(arg(e, 0)); }
-inline expr mk_eq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eq_fn(), e1, e2, e3}); }
-expr mk_neq_fn();
-bool is_neq_fn(expr const & e);
-inline bool is_neq(expr const & e) { return is_app(e) && is_neq_fn(arg(e, 0)); }
-inline expr mk_neq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_fn(), e1, e2, e3}); }
 expr mk_em_fn();
 bool is_em_fn(expr const & e);
 inline expr mk_em_th(expr const & e1) { return mk_app({mk_em_fn(), e1}); }
@@ -151,15 +149,6 @@ inline expr mk_eq_ne_trans_th(expr const & e1, expr const & e2, expr const & e3,
 expr mk_ne_eq_trans_fn();
 bool is_ne_eq_trans_fn(expr const & e);
 inline expr mk_ne_eq_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_ne_eq_trans_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_heq_congr_fn();
-bool is_heq_congr_fn(expr const & e);
-inline expr mk_heq_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_heq_congr_fn(), e1, e2, e3, e4, e5, e6, e7}); }
-expr mk_heq_congrl_fn();
-bool is_heq_congrl_fn(expr const & e);
-inline expr mk_heq_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_heq_congrl_fn(), e1, e2, e3, e4, e5}); }
-expr mk_heq_congrr_fn();
-bool is_heq_congrr_fn(expr const & e);
-inline expr mk_heq_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_heq_congrr_fn(), e1, e2, e3, e4, e5}); }
 expr mk_eqt_elim_fn();
 bool is_eqt_elim_fn(expr const & e);
 inline expr mk_eqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_elim_fn(), e1, e2}); }
@@ -175,12 +164,6 @@ inline expr mk_congr2_th(expr const & e1, expr const & e2, expr const & e3, expr
 expr mk_congr_fn();
 bool is_congr_fn(expr const & e);
 inline expr mk_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
-expr mk_scongr2_fn();
-bool is_scongr2_fn(expr const & e);
-inline expr mk_scongr2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_scongr2_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_scongr_fn();
-bool is_scongr_fn(expr const & e);
-inline expr mk_scongr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_scongr_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
 expr mk_exists_elim_fn();
 bool is_exists_elim_fn(expr const & e);
 inline expr mk_exists_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_exists_elim_fn(), e1, e2, e3, e4, e5}); }

src/kernel/max_sharing.cpp

@@ -56,11 +56,6 @@ struct max_sharing_fn::imp {
             cache(r);
             return r;
         }
-        case expr_kind::HEq : {
-            expr r = update_heq(a, [=](expr const & l, expr const & r) { return std::make_pair(apply(l), apply(r)); });
-            cache(r);
-            return r;
-        }
         case expr_kind::Lambda:
         case expr_kind::Pi: {
             expr r = update_abst(a, [=](expr const & t, expr const & b) { return std::make_pair(apply(t), apply(b)); });

src/kernel/normalizer.cpp

@@ -309,16 +309,6 @@ class normalizer::imp {
             }
             break;
         }
-        case expr_kind::HEq: {
-            expr new_lhs = normalize(heq_lhs(a), s, k);
-            expr new_rhs = normalize(heq_rhs(a), s, k);
-            if (is_value(new_lhs) && is_value(new_rhs) && !is_closure(new_lhs) && !is_closure(new_rhs) && typeid(to_value(new_lhs)) == typeid(to_value(new_rhs))) {
-                r = mk_bool_value(new_lhs == new_rhs);
-            } else {
-                r = mk_heq(new_lhs, new_rhs);
-            }
-            break;
-        }
         case expr_kind::Let: {
             expr v = normalize(let_value(a), s, k);
             {

src/kernel/replace_fn.h

@@ -156,14 +156,6 @@ public:
                 pop_rs(num);
                 break;
             }
-            case expr_kind::HEq:
-                if (check_index(f, 0) && !visit(heq_lhs(e), offset))
-                    goto begin_loop;
-                if (check_index(f, 1) && !visit(heq_rhs(e), offset))
-                    goto begin_loop;
-                r = update_heq(e, rs(-2), rs(-1));
-                pop_rs(2);
-                break;
             case expr_kind::Pi: case expr_kind::Lambda:
                 if (check_index(f, 0) && !visit(abst_domain(e), offset))
                     goto begin_loop;

src/kernel/replace_visitor.cpp

@@ -22,10 +22,6 @@ expr replace_visitor::visit_app(expr const & e, context const & ctx) {
     lean_assert(is_app(e));
     return update_app(e, [&](expr const & c) { return visit(c, ctx); });
 }
-expr replace_visitor::visit_heq(expr const & e, context const & ctx) {
-    lean_assert(is_heq(e));
-    return update_heq(e, [&](expr const & l, expr const & r) { return std::make_pair(visit(l, ctx), visit(r, ctx)); });
-}
 expr replace_visitor::visit_abst(expr const & e, context const & ctx) {
     lean_assert(is_abstraction(e));
     return update_abst(e, [&](expr const & t, expr const & b) {
@@ -80,7 +76,6 @@ expr replace_visitor::visit(expr const & e, context const & ctx) {
     case expr_kind::Var:       return save_result(e, visit_var(e, ctx), shared);
     case expr_kind::MetaVar:   return save_result(e, visit_metavar(e, ctx), shared);
     case expr_kind::App:       return save_result(e, visit_app(e, ctx), shared);
-    case expr_kind::HEq:       return save_result(e, visit_heq(e, ctx), shared);
     case expr_kind::Lambda:    return save_result(e, visit_lambda(e, ctx), shared);
     case expr_kind::Pi:        return save_result(e, visit_pi(e, ctx), shared);
     case expr_kind::Let:       return save_result(e, visit_let(e, ctx), shared);

src/kernel/replace_visitor.h

@@ -31,7 +31,6 @@ protected:
     virtual expr visit_var(expr const &, context const &);
     virtual expr visit_metavar(expr const &, context const &);
     virtual expr visit_app(expr const &, context const &);
-    virtual expr visit_heq(expr const &, context const &);
     virtual expr visit_abst(expr const &, context const &);
     virtual expr visit_lambda(expr const &, context const &);
     virtual expr visit_pi(expr const &, context const &);

src/kernel/type_checker.cpp

@@ -48,7 +48,7 @@ class type_checker::imp {
             return u;
         if (has_metavar(u) && m_menv && m_uc) {
             justification jst = mk_type_expected_justification(ctx, s);
-            m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU, jst));
+            m_uc->push_back(mk_convertible_constraint(ctx, e, TypeUp, jst));
             return u;
         }
         u = normalize(e, ctx, true);
@@ -176,10 +176,6 @@ class type_checker::imp {
             }
         case expr_kind::Type:
             return mk_type(ty_level(e) + 1);
-        case expr_kind::HEq:
-            // cheap when we are just inferring types
-            if (m_infer_only)
-                return mk_bool_type();
         case expr_kind::App: case expr_kind::Lambda:
         case expr_kind::Pi:  case expr_kind::Let:
             break; // expensive cases
@@ -241,11 +237,6 @@ class type_checker::imp {
                     f_t = check_pi(f_t, e, ctx);
                 }
             }
-        case expr_kind::HEq:
-            lean_assert(!m_infer_only);
-            infer_type_core(heq_lhs(e), ctx);
-            infer_type_core(heq_rhs(e), ctx);
-            return save_result(e, mk_bool_type(), shared);
         case expr_kind::Lambda:
             if (!m_infer_only) {
                 expr d = infer_type_core(abst_domain(e), ctx);
@@ -423,8 +414,6 @@ public:
         switch (e.kind()) {
         case expr_kind::Lambda: case expr_kind::Type:
             return false;
-        case expr_kind::HEq:
-            return true;
         case expr_kind::Pi:
             return is_proposition(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)), menv);
         default:

src/kernel/update_expr.cpp

@@ -66,11 +66,4 @@ expr update_let(expr const & let, optional<expr> const & t, expr const & v, expr
     else
         return mk_let(let_name(let), t, v, b);
 }
-
-expr update_heq(expr const & eq, expr const & l, expr const & r) {
-    if (is_eqp(heq_lhs(eq), l) && is_eqp(heq_rhs(eq), r))
-        return eq;
-    else
-        return mk_heq(l, r);
-}
 }

src/library/deep_copy.cpp

@@ -43,7 +43,6 @@ class deep_copy_fn {
                 new_args.push_back(apply(old_arg));
             return save_result(a, mk_app(new_args), sh);
         }
-        case expr_kind::HEq:      return save_result(a, mk_heq(apply(heq_lhs(a)), apply(heq_rhs(a))), sh);
         case expr_kind::Lambda:   return save_result(a, mk_lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh);
         case expr_kind::Pi:       return save_result(a, mk_pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh);
         case expr_kind::Let:      return save_result(a, mk_let(let_name(a), apply(let_type(a)), apply(let_value(a)), apply(let_body(a))), sh);

src/library/elaborator/elaborator.cpp

@@ -620,18 +620,11 @@ class elaborator::imp {
         }
     }
 
-    void process_eq(context const & ctx, expr & a) {
-        if (is_heq(a) && m_use_normalizer) {
-            a = normalize(ctx, a);
-        }
-    }
-
     expr normalize_step(context const & ctx, expr const & a) {
         expr new_a = a;
         process_let(new_a);
         process_var(ctx, new_a);
         process_app(ctx, new_a);
-        process_eq(ctx, new_a);
         return new_a;
     }
 
@@ -840,17 +833,6 @@ class elaborator::imp {
                 push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_i), arg(b, i), new_assumption);
             }
             imitation = mk_lambda(arg_types, mk_app(imitation_args));
-        } else if (is_heq(b)) {
-            // Imitation for equality
-            // Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), (h_1 x_1 ... x_{num_a}) = (h_2 x_1 ... x_{num_a})
-            // New constraints (h_1 a_1 ... a_{num_a}) == eq_lhs(b)
-            //                 (h_2 a_1 ... a_{num_a}) == eq_rhs(b)
-            expr h_1 = new_state.m_menv->mk_metavar(ctx);
-            expr h_2 = new_state.m_menv->mk_metavar(ctx);
-            push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_1), heq_lhs(b), new_assumption);
-            push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_2), heq_rhs(b), new_assumption);
-            imitation = mk_lambda(arg_types, mk_heq(mk_app_vars(add_lift(h_1, 0, num_a - 1), num_a - 1),
-                                                    mk_app_vars(add_lift(h_2, 0, num_a - 1), num_a - 1)));
         } else if (is_abstraction(b)) {
             // Imitation for lambdas and Pis
             // Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}),
@@ -1058,28 +1040,6 @@ class elaborator::imp {
         }
     }
 
-    /**
-       \brief Similar to imitate_abstraction, but b is a heterogeneous equality.
-    */
-    void imitate_equality(expr const & a, expr const & b, unification_constraint const & c) {
-        lean_assert(is_metavar(a));
-        static_cast<void>(b); // this line is just to avoid a warning, b is only used in an assertion
-        lean_assert(is_heq(b));
-        lean_assert(!is_assigned(a));
-        lean_assert(has_local_context(a));
-        // imitate
-        push_active(c);
-        // Create a fresh meta variable for the lhs and rhs of b.
-        // The new metavariables have the same context of a.
-        expr m         = mk_metavar(metavar_name(a));
-        context ctx_m  = m_state.m_menv->get_context(m);
-        expr h1        = m_state.m_menv->mk_metavar(ctx_m);
-        expr h2        = m_state.m_menv->mk_metavar(ctx_m);
-        expr imitation = mk_heq(h1, h2);
-        justification new_jst(new imitation_justification(c));
-        push_new_constraint(true, ctx_m, m, imitation, new_jst);
-    }
-
     /**
        \brief Process a constraint <tt>ctx |- a == b</tt> where \c a is of the form <tt>?m[(inst:i t), ...]</tt>.
        We perform a "case split",
@@ -1138,9 +1098,6 @@ class elaborator::imp {
             } else if (is_app(b) && !has_metavar(arg(b, 0))) {
                 imitate_application(a, b, c);
                 return true;
-            } else if (is_heq(b)) {
-                imitate_equality(a, b, c);
-                return true;
             }
         }
         return false;
@@ -1179,16 +1136,16 @@ class elaborator::imp {
             // We approximate and only consider the most useful ones.
             justification new_jst(new destruct_justification(c));
             if (is_bool(a)) {
-                expr choices[3] = { Bool, Type(), TypeU };
+                expr choices[4] = { Bool, Type(), TypeU, TypeUp };
-                push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst));
+                push_active(mk_choice_constraint(get_context(c), b, 4, choices, new_jst));
                 return true;
             } else if (m_env->is_ge(ty_level(a), m_U)) {
-                expr choices[2] = { a, Type(ty_level(a) + 1) };
+                expr choices[3] = { a, Type(ty_level(a) + 1), TypeUp };
-                push_active(mk_choice_constraint(get_context(c), b, 2, choices, new_jst));
+                push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst));
                 return true;
             } else {
-                expr choices[3] = { a, Type(ty_level(a) + 1), TypeU };
+                expr choices[4] = { a, Type(ty_level(a) + 1), TypeU };
-                push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst));
+                push_active(mk_choice_constraint(get_context(c), b, 4, choices, new_jst));
                 return true;
             }
         } else {
@@ -1253,6 +1210,10 @@ class elaborator::imp {
                 expr choices[4] = { TypeU, Type(level() + 1), Type(), Bool };
                 push_active(mk_choice_constraint(get_context(c), a, 4, choices, new_jst));
                 return true;
+            } else if (b == TypeUp) {
+                expr choices[5] = { TypeUp, TypeU, Type(level() + 1), Type(), Bool };
+                push_active(mk_choice_constraint(get_context(c), a, 5, choices, new_jst));
+                return true;
             } else {
                 level const & lvl = ty_level(b);
                 lean_assert(!lvl.is_bottom());
@@ -1376,6 +1337,8 @@ class elaborator::imp {
             expr_pair p1 = get_equality_args(a);
             expr_pair p2 = get_equality_args(b);
             justification new_jst(new destruct_justification(c));
+            if (is_eq(a) && is_eq(b))
+                push_new_eq_constraint(ctx, arg(a, 1), arg(b, 1), new_jst);
             push_new_eq_constraint(ctx, p1.first,  p2.first,  new_jst);
             push_new_eq_constraint(ctx, p1.second, p2.second, new_jst);
             return true;

src/library/equality.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 bool is_equality(expr const & e) {
-    return is_eq(e) || is_iff(e) || is_heq(e);
+    return is_eq(e) || is_iff(e);
 }
 
 bool is_equality(expr const & e, expr & lhs, expr & rhs) {
@@ -21,10 +21,6 @@ bool is_equality(expr const & e, expr & lhs, expr & rhs) {
         lhs = arg(e, 1);
         rhs = arg(e, 2);
         return true;
-    } else if (is_heq(e)) {
-        lhs = heq_lhs(e);
-        rhs = heq_rhs(e);
-        return true;
     } else {
         return false;
     }
@@ -35,8 +31,6 @@ expr_pair get_equality_args(expr const & e) {
         return mk_pair(arg(e, 2), arg(e, 3));
     } else if (is_iff(e)) {
         return mk_pair(arg(e, 1), arg(e, 2));
-    } else if (is_heq(e)) {
-        return mk_pair(heq_lhs(e), heq_rhs(e));
     } else {
         lean_unreachable(); // LCOV_EXCL_LINE
     }

src/library/expr_lt.cpp

@@ -37,11 +37,6 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) {
                 return is_lt(arg(a, i), arg(b, i), use_hash);
         }
         lean_unreachable(); // LCOV_EXCL_LINE
-    case expr_kind::HEq:
-        if (heq_lhs(a) != heq_lhs(b))
-            return is_lt(heq_lhs(a), heq_lhs(b), use_hash);
-        else
-            return is_lt(heq_rhs(a), heq_rhs(b), use_hash);
     case expr_kind::Lambda:   // Remark: we ignore get_abs_name because we want alpha-equivalence
     case expr_kind::Pi:
         if (abst_domain(a) != abst_domain(b))

src/library/fo_unify.cpp

@@ -62,8 +62,6 @@ optional<substitution> fo_unify(expr e1, expr e2) {
                         }
                     }
                     break;
-                case expr_kind::HEq:
-                    lean_unreachable(); break; // LCOV_EXCL_LINE
                 case expr_kind::Lambda: case expr_kind::Pi:
                     todo.emplace_back(abst_body(e1), abst_body(e2));
                     todo.emplace_back(abst_domain(e1), abst_domain(e2));

src/library/hop_match.cpp

@@ -216,8 +216,6 @@ class hop_match_fn {
                 }
                 return true;
             }
-            case expr_kind::HEq:
-                lean_unreachable(); break; // LCOV_EXCL_LINE
             case expr_kind::Lambda: case expr_kind::Pi:
                 return
                     match(abst_domain(p), abst_domain(t), ctx, ctx_size) &&

src/library/kernel_bindings.cpp

@@ -323,10 +323,6 @@ static int expr_mk_app(lua_State * L) {
     return push_expr(L, mk_app(args));
 }
 
-static int expr_mk_heq(lua_State * L) {
-    return push_expr(L, mk_heq(to_expr(L, 1), to_expr(L, 2)));
-}
-
 static int expr_mk_lambda(lua_State * L) {
     return push_expr(L, mk_lambda(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3)));
 }
@@ -438,7 +434,6 @@ static int expr_ ## P(lua_State * L) {                  \
 EXPR_PRED(is_constant)
 EXPR_PRED(is_var)
 EXPR_PRED(is_app)
-EXPR_PRED(is_heq)
 EXPR_PRED(is_lambda)
 EXPR_PRED(is_pi)
 EXPR_PRED(is_abstraction)
@@ -500,7 +495,6 @@ static int expr_fields(lua_State * L) {
     case expr_kind::Type:     return push_level(L, ty_level(e));
     case expr_kind::Value:    return to_value(e).push_lua(L);
     case expr_kind::App:      lua_pushinteger(L, num_args(e)); expr_args(L); return 2;
-    case expr_kind::HEq:      push_expr(L, heq_lhs(e)); push_expr(L, heq_rhs(e)); return 2;
     case expr_kind::Lambda:
     case expr_kind::Pi:
         push_name(L, abst_name(e)); push_expr(L, abst_domain(e)); push_expr(L, abst_body(e)); return 3;
@@ -633,6 +627,10 @@ static int expr_abst_body(lua_State * L) {
     return push_expr(L, abst_body(to_expr(L, 1)));
 }
 
+static int expr_mk_eq(lua_State * L) {
+    return push_expr(L, mk_eq(to_expr(L, 1), to_expr(L, 2), to_expr(L, 3)));
+}
+
 static const struct luaL_Reg expr_m[] = {
     {"__gc",             expr_gc}, // never throws
     {"__tostring",       safe_function<expr_tostring>},
@@ -643,7 +641,6 @@ static const struct luaL_Reg expr_m[] = {
     {"is_var",           safe_function<expr_is_var>},
     {"is_constant",      safe_function<expr_is_constant>},
     {"is_app",           safe_function<expr_is_app>},
-    {"is_heq",           safe_function<expr_is_heq>},
     {"is_lambda",       safe_function<expr_is_lambda>},
     {"is_pi",            safe_function<expr_is_pi>},
     {"is_abstraction",   safe_function<expr_is_abstraction>},
@@ -697,8 +694,6 @@ static void open_expr(lua_State * L) {
     SET_GLOBAL_FUN(expr_mk_var,      "mk_var");
     SET_GLOBAL_FUN(expr_mk_var,      "Var");
     SET_GLOBAL_FUN(expr_mk_app,      "mk_app");
-    SET_GLOBAL_FUN(expr_mk_heq,      "mk_heq");
-    SET_GLOBAL_FUN(expr_mk_heq,      "HEq");
     SET_GLOBAL_FUN(expr_mk_lambda,   "mk_lambda");
     SET_GLOBAL_FUN(expr_mk_pi,       "mk_pi");
     SET_GLOBAL_FUN(expr_mk_arrow,    "mk_arrow");
@@ -708,6 +703,7 @@ static void open_expr(lua_State * L) {
     SET_GLOBAL_FUN(expr_pi,          "Pi");
     SET_GLOBAL_FUN(expr_let,         "Let");
     SET_GLOBAL_FUN(expr_type,        "mk_type");
+    SET_GLOBAL_FUN(expr_mk_eq,       "mk_eq");
     SET_GLOBAL_FUN(expr_type,        "Type");
     SET_GLOBAL_FUN(expr_mk_metavar,  "mk_metavar");
     SET_GLOBAL_FUN(expr_pred,        "is_expr");
@@ -718,7 +714,6 @@ static void open_expr(lua_State * L) {
     SET_ENUM("Type",     expr_kind::Type);
     SET_ENUM("Value",    expr_kind::Value);
     SET_ENUM("App",      expr_kind::App);
-    SET_ENUM("HEq",      expr_kind::HEq);
     SET_ENUM("Lambda",   expr_kind::Lambda);
     SET_ENUM("Pi",       expr_kind::Pi);
     SET_ENUM("Let",      expr_kind::Let);

src/library/printer.cpp

@@ -18,7 +18,7 @@ bool is_atomic(expr const & e) {
     case expr_kind::Type: case expr_kind::MetaVar:
         return true;
     case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi:
-    case expr_kind::HEq: case expr_kind::Let:
+    case expr_kind::Let:
         return false;
     }
     return false;
@@ -55,12 +55,6 @@ struct print_expr_fn {
         }
     }
 
-    void print_heq(expr const & a, context const & c) {
-        print_child(heq_lhs(a), c);
-        out() << " == ";
-        print_child(heq_rhs(a), c);
-    }
-
     void print_app(expr const & e, context const & c) {
         print_child(arg(e, 0), c);
         for (unsigned i = 1; i < num_args(e); i++) {
@@ -114,9 +108,6 @@ struct print_expr_fn {
         case expr_kind::App:
             print_app(a, c);
             break;
-        case expr_kind::HEq:
-            print_heq(a, c);
-            break;
         case expr_kind::Lambda:
             out() << "fun " << abst_name(a) << " : ";
             print_child(abst_domain(a), c);

src/library/rewriter/fo_match.cpp

@@ -117,13 +117,6 @@ bool fo_match::match_type(expr const & p, expr const & t, unsigned, subst_map &)
     return p == t;
 }
 
-bool fo_match::match_heq(expr const & p, expr const & t, unsigned o, subst_map & s) {
-    lean_trace("fo_match", tout << "match_eq : (" << p << ", " << t << ", " << o << ", " << s << ")" << endl;); // LCOV_EXCL_LINE
-    if (!is_heq(t))
-        return false;
-    return match_main(heq_lhs(p), heq_lhs(t), o, s) && match_main(heq_rhs(p), heq_rhs(t), o, s);
-}
-
 bool fo_match::match_let(expr const & p, expr const & t, unsigned o, subst_map & s) {
     lean_trace("fo_match", tout << "match_let : (" << p << ", " << t << ", " << o << ", " << s << ")" << endl;); // LCOV_EXCL_LINE
     if (!is_let(t)) {
@@ -176,8 +169,6 @@ bool fo_match::match_main(expr const & p, expr const & t, unsigned o, subst_map
         return match_pi(p, t, o, s);
     case expr_kind::Type:
         return match_type(p, t, o, s);
-    case expr_kind::HEq:
-        return match_heq(p, t, o, s);
     case expr_kind::Let:
         return match_let(p, t, o, s);
     case expr_kind::MetaVar:

src/library/rewriter/fo_match.h

@@ -22,7 +22,6 @@ private:
     bool match_lambda(expr const & p, expr const & t, unsigned o, subst_map & s);
     bool match_pi(expr const & p, expr const & t, unsigned o, subst_map & s);
     bool match_type(expr const & p, expr const & t, unsigned o, subst_map & s);
-    bool match_heq(expr const & p, expr const & t, unsigned o, subst_map & s);
     bool match_let(expr const & p, expr const & t, unsigned o, subst_map & s);
     bool match_metavar(expr const & p, expr const & t, unsigned o, subst_map & s);
     bool match_main(expr const & p, expr const & t, unsigned o, subst_map & s);

src/library/rewriter/rewriter.cpp

@@ -51,14 +51,17 @@ pair<expr, expr> rewrite_lambda_type(environment const & env, context & ctx, exp
     } else {
         name const & n         = abst_name(v);
         expr const & body      = abst_body(v);
-        expr const & pf_ty     = result_ty.second;
+        // expr const & pf_ty     = result_ty.second;
         expr const & new_v     = mk_lambda(n, new_ty, body);
         expr const & ty_ty     = ti(ty, ctx);
         lean_assert_eq(ty_ty, ti(new_ty, ctx)); // TODO(soonhok): generalize for hetreogeneous types
-        expr const & proof     = mk_subst_th(ty_ty, ty, new_ty,
+        expr proof;
-                                       Fun({Const("T"), ty_ty},
+#if 0  // TODO(Leo): we don't have heterogeneous equality anymore
-                                           mk_heq(v, mk_lambda(n, Const("T"), body))),
+            = mk_subst_th(ty_ty, ty, new_ty,
-                                       mk_refl_th(ty_v, v), pf_ty);
+                          Fun({Const("T"), ty_ty},
+                              mk_heq(v, mk_lambda(n, Const("T"), body))),
+                          mk_refl_th(ty_v, v), pf_ty);
+#endif
         return make_pair(new_v, proof);
     }
 }
@@ -111,35 +114,38 @@ pair<expr, expr> rewrite_lambda_body(environment const & env, context & ctx, exp
           body')
    \return pair of v' = \f$(\lambda n : ty'. body')\f$, and proof of v = v'
 */
-pair<expr, expr> rewrite_lambda(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_ty, pair<expr, expr> const & result_body) {
+pair<expr, expr> rewrite_lambda(environment const & env, context & /* ctx */,  expr const & v, pair<expr, expr> const & result_ty, pair<expr, expr> const & result_body) {
     lean_assert(is_lambda(v));
     type_inferer ti(env);
     name const & n         = abst_name(v);
-    expr const & ty        = abst_domain(v);
+    // expr const & ty        = abst_domain(v);
-    expr const & body      = abst_body(v);
+    // expr const & body      = abst_body(v);
     expr const & new_ty    = result_ty.first;
-    expr const & pf_ty     = result_ty.second;
+    // expr const & pf_ty     = result_ty.second;
     expr const & new_body  = result_body.first;
-    expr const & pf_body   = result_body.second;
+    // expr const & pf_body   = result_body.second;
-    expr const & ty_ty     = ti(ty, ctx);
+    // expr const & ty_ty     = ti(ty, ctx);
-    expr const & ty_body   = ti(body, ctx);
+    // expr const & ty_body   = ti(body, ctx);
-    expr const & ty_v      = ti(v, ctx);
+    // expr const & ty_v      = ti(v, ctx);
-    expr const & new_v1    = mk_lambda(n, new_ty, body);
+    // expr const & new_v1    = mk_lambda(n, new_ty, body);
-    expr const & ty_new_v1 = ti(v, ctx);
+    // expr const & ty_new_v1 = ti(v, ctx);
     expr const & new_v2    = mk_lambda(n, new_ty, new_body);
     // proof1 : v = new_v1
-    expr const & proof1    = mk_subst_th(ty_ty, ty, new_ty,
+
+    expr proof;
+#if 0 // TODO(Leo): we don't have heterogeneous equality anymore
+    expr proof1 = mk_subst_th(ty_ty, ty, new_ty,
                                          Fun({Const("T"), ty_ty},
                                              mk_heq(v, mk_lambda(n, Const("T"), body))),
                                          mk_refl_th(ty_v, v),
                                          pf_ty);
-    // proof2 : new_v1 = new_v2
+    expr proof2 = mk_subst_th(ty_body, body, new_body,
-    expr const & proof2    = mk_subst_th(ty_body, body, new_body,
                                          Fun({Const("e"), ty_body},
                                              mk_heq(new_v1, mk_lambda(n, new_ty, Const("e")))),
                                          mk_refl_th(ty_new_v1, new_v1),
                                          pf_body);
     expr const & proof     = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2);
+#endif
     return make_pair(new_v2, proof);
 }
 
@@ -155,22 +161,25 @@ pair<expr, expr> rewrite_lambda(environment const & env, context & ctx, expr con
           rewritten type of ty and pf_ty the proof of (ty = ty')
    \return pair of v' = \f$(\Pi n : ty'. body)\f$, and proof of v = v'
 */
-pair<expr, expr> rewrite_pi_type(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_ty) {
+pair<expr, expr> rewrite_pi_type(environment const & env, context & /* ctx */, expr const & v, pair<expr, expr> const & result_ty) {
     lean_assert(is_pi(v));
     type_inferer ti(env);
     name const & n      = abst_name(v);
-    expr const & ty     = abst_domain(v);
+    // expr const & ty     = abst_domain(v);
     expr const & body   = abst_body(v);
     expr const & new_ty = result_ty.first;
-    expr const & pf     = result_ty.second;
+    // expr const & pf     = result_ty.second;
     expr const & new_v  = mk_pi(n, new_ty, body);
-    expr const & ty_ty  = ti(ty, ctx);
+    // expr const & ty_ty  = ti(ty, ctx);
-    expr const & ty_v   = ti(v, ctx);
+    // expr const & ty_v   = ti(v, ctx);
-    expr const & proof  = mk_subst_th(ty_ty, ty, new_ty,
+    expr proof;
+#if 0 // TODO(Leo): HEq is gone
+    = mk_subst_th(ty_ty, ty, new_ty,
                                       Fun({Const("T"), ty_ty},
                                           mk_heq(v, mk_pi(n, Const("T"), body))),
                                       mk_refl_th(ty_v, v),
                                       pf);
+#endif
     return make_pair(new_v, proof);
 }
 
@@ -187,22 +196,25 @@ pair<expr, expr> rewrite_pi_type(environment const & env, context & ctx, expr co
           body')
    \return pair of v' = \f$(\Pi n : ty. body')\f$, and proof of v = v'
 */
-pair<expr, expr> rewrite_pi_body(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_body) {
+pair<expr, expr> rewrite_pi_body(environment const & env, context & /* ctx */, expr const & v, pair<expr, expr> const & result_body) {
     lean_assert(is_pi(v));
     type_inferer ti(env);
     name const & n        = abst_name(v);
     expr const & ty       = abst_domain(v);
-    expr const & body     = abst_body(v);
+    // expr const & body     = abst_body(v);
     expr const & new_body = result_body.first;
-    expr const & pf       = result_body.second;
+    // expr const & pf       = result_body.second;
     expr const & new_v    = mk_pi(n, ty, new_body);
-    expr const & ty_body  = ti(body, extend(ctx, n, ty));
+    // expr const & ty_body  = ti(body, extend(ctx, n, ty));
-    expr const & ty_v     = ti(v, ctx);
+    // expr const & ty_v     = ti(v, ctx);
+    expr proof;
+#if 0 // TODO(Leo): HEq is gone
     expr const & proof    = mk_subst_th(ty_body, body, new_body,
                                   Fun({Const("e"), ty_body},
                                       mk_heq(v, mk_pi(n, ty, Const("e")))),
                                   mk_refl_th(ty_v, v),
                                   pf);
+#endif
     return make_pair(new_v, proof);
 }
 
@@ -221,22 +233,24 @@ pair<expr, expr> rewrite_pi_body(environment const & env, context & ctx, expr co
           body')
    \return pair of v' = \f$(\Pi n : ty'. body')\f$, and proof of v = v'
 */
-pair<expr, expr> rewrite_pi(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_ty, pair<expr, expr> const & result_body) {
+pair<expr, expr> rewrite_pi(environment const & env, context & /*ctx*/, expr const & v, pair<expr, expr> const & result_ty, pair<expr, expr> const & result_body) {
     lean_assert(is_pi(v));
     type_inferer ti(env);
     name const & n         = abst_name(v);
-    expr const & ty        = abst_domain(v);
+    // expr const & ty        = abst_domain(v);
-    expr const & body      = abst_body(v);
+    // expr const & body      = abst_body(v);
     expr const & new_ty    = result_ty.first;
-    expr const & pf_ty     = result_ty.second;
+    // expr const & pf_ty     = result_ty.second;
     expr const & new_body  = result_body.first;
-    expr const & pf_body   = result_body.second;
+    // expr const & pf_body   = result_body.second;
-    expr const & ty_ty     = ti(ty, ctx);
+    // expr const & ty_ty     = ti(ty, ctx);
-    expr const & ty_body   = ti(body, ctx);
+    // expr const & ty_body   = ti(body, ctx);
-    expr const & ty_v      = ti(v, ctx);
+    // expr const & ty_v      = ti(v, ctx);
-    expr const & new_v1    = mk_pi(n, new_ty, body);
+    // expr const & new_v1    = mk_pi(n, new_ty, body);
-    expr const & ty_new_v1 = ti(v, ctx);
+    // expr const & ty_new_v1 = ti(v, ctx);
     expr const & new_v2    = mk_pi(n, new_ty, new_body);
+    expr proof;
+#if 0 // TODO(Leo): HEq is gone
     expr const & proof1    = mk_subst_th(ty_ty, ty, new_ty,
                                    Fun({Const("T"), ty_ty},
                                        mk_heq(v, mk_pi(n, Const("T"), body))),
@@ -248,109 +262,7 @@ pair<expr, expr> rewrite_pi(environment const & env, context & ctx, expr const &
                                    mk_refl_th(ty_new_v1, new_v1),
                                    pf_body);
     expr const & proof     = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2);
-    return make_pair(new_v2, proof);
+#endif
-}
-
-/**
-   \brief For a Eq term v = (lhs = rhs) and the rewriting result for
-   lhs, it constructs a new rewriting result for v' = (lhs' = rhs)
-   with the proof of v = v'.
-
-   \param env environment
-   \param ctx context
-   \param v (lhs = rhs)
-   \param result_lhs rewriting result of lhs -- pair of lhs'
-          rewritten term of lhs and pf_lhs the proof of (lhs = lhs')
-   \return pair of v' = (lhs' = rhs), and proof of v = v'
-*/
-pair<expr, expr> rewrite_eq_lhs(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_lhs) {
-    lean_assert(is_heq(v));
-    type_inferer ti(env);
-    expr const & lhs     = heq_lhs(v);
-    expr const & rhs     = heq_rhs(v);
-    expr const & new_lhs = result_lhs.first;
-    expr const & pf      = result_lhs.second;
-    expr const & new_v   = mk_heq(new_lhs, rhs);
-    expr const & ty_lhs  = ti(lhs, ctx);
-    expr const & ty_v    = ti(v, ctx);
-    expr const & proof   = mk_subst_th(ty_lhs, lhs, new_lhs,
-                                 Fun({Const("x"), ty_lhs},
-                                     mk_heq(v, mk_heq(Const("x"), rhs))),
-                                 mk_refl_th(ty_v, v),
-                                 pf);
-    return make_pair(new_v, proof);
-}
-
-/**
-   \brief For a Eq term v = (lhs = rhs)and the rewriting
-   result for rhs, it constructs a new rewriting result for v'
-   = (lhs = rhs') with the proof of v = v'.
-
-   \param env environment
-   \param ctx context
-   \param v (lhs = rhs)
-   \param result_rhs rewriting result of rhs -- pair of rhs'
-          rewritten term of rhs and pf_rhs the proof of (rhs = rhs')
-   \return pair of v' = (lhs = rhs'), and proof of v = v'
-*/
-pair<expr, expr> rewrite_eq_rhs(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_rhs) {
-    lean_assert(is_heq(v));
-    type_inferer ti(env);
-    expr const & lhs     = heq_lhs(v);
-    expr const & rhs     = heq_rhs(v);
-    expr const & new_rhs = result_rhs.first;
-    expr const & pf      = result_rhs.second;
-    expr const & new_v   = mk_heq(rhs, new_rhs);
-    expr const & ty_rhs  = ti(rhs, ctx);
-    expr const & ty_v    = ti(v, ctx);
-    expr const & proof   = mk_subst_th(ty_rhs, rhs, new_rhs,
-                                 Fun({Const("x"), ty_rhs},
-                                     mk_heq(v, mk_heq(lhs, Const("x")))),
-                                 mk_refl_th(ty_v, v),
-                                 pf);
-    return make_pair(new_v, proof);
-}
-
-/**
-   \brief For a Eq term v = (lhs = rhs)and the rewriting result for
-   lhs and rhs, it constructs a new rewriting result for v' = (lhs' =
-   rhs') with the proof of v = v'.
-
-   \param env environment
-   \param ctx context
-   \param v (lhs = rhs)
-   \param result_lhs rewriting result of lhs -- pair of lhs'
-          rewritten term of lhs and pf_lhs the proof of (lhs = lhs')
-   \param result_rhs rewriting result of rhs -- pair of rhs'
-          rewritten term of rhs and pf_rhs the proof of (rhs = rhs')
-   \return pair of v' = (lhs' = rhs'), and proof of v = v'
-*/
-pair<expr, expr> rewrite_eq(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_lhs, pair<expr, expr> const & result_rhs) {
-    lean_assert(is_heq(v));
-    type_inferer ti(env);
-    expr const & lhs       = heq_lhs(v);
-    expr const & rhs       = heq_rhs(v);
-    expr const & new_lhs   = result_lhs.first;
-    expr const & pf_lhs    = result_lhs.second;
-    expr const & new_rhs   = result_rhs.first;
-    expr const & pf_rhs    = result_rhs.second;
-    expr const & new_v1    = mk_heq(new_lhs, rhs);
-    expr const & new_v2    = mk_heq(new_lhs, new_rhs);
-    expr const & ty_lhs    = ti(lhs, ctx);
-    expr const & ty_rhs    = ti(rhs, ctx);
-    expr const & ty_v      = ti(v, ctx);
-    expr const & ty_new_v1 = ti(new_v1, ctx);
-    expr const & proof1 = mk_subst_th(ty_lhs, lhs, new_lhs,
-                                Fun({Const("x"), ty_lhs},
-                                    mk_heq(v, mk_heq(Const("x"), rhs))),
-                                mk_refl_th(ty_v, v),
-                                pf_lhs);
-    expr const & proof2 = mk_subst_th(ty_rhs, rhs, new_rhs,
-                                Fun({Const("x"), ty_rhs},
-                                    mk_heq(v, mk_heq(lhs, Const("x")))),
-                                mk_refl_th(ty_new_v1, new_v1),
-                                pf_rhs);
-    expr const & proof  = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2);
     return make_pair(new_v2, proof);
 }
 
@@ -366,24 +278,27 @@ pair<expr, expr> rewrite_eq(environment const & env, context & ctx, expr const &
           rewritten type of ty and \c pf_ty the proof of (ty = ty')
    \return pair of v' = (let n : ty' = val in body), and proof of v = v'
 */
-pair<expr, expr> rewrite_let_type(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_ty) {
+pair<expr, expr> rewrite_let_type(environment const & env, context & /* ctx */, expr const & v, pair<expr, expr> const & result_ty) {
     lean_assert(is_let(v));
     type_inferer ti(env);
     if (!let_type(v)) {
         name const & n       = let_name(v);
-        expr const & ty      = *let_type(v);
+        // expr const & ty      = *let_type(v);
         expr const & val     = let_value(v);
         expr const & body    = let_body(v);
         expr const & new_ty  = result_ty.first;
-        expr const & pf      = result_ty.second;
+        // expr const & pf      = result_ty.second;
         expr const & new_v   = mk_let(n, new_ty, val, body);
-        expr const & ty_ty   = ti(ty, ctx);
+        // expr const & ty_ty   = ti(ty, ctx);
-        expr const & ty_v    = ti(v, ctx);
+        // expr const & ty_v    = ti(v, ctx);
+        expr proof;
+#if 0 // TODO(Leo): HEq is gone
         expr const & proof   = mk_subst_th(ty_ty, ty, new_ty,
                                      Fun({Const("x"), ty_ty},
                                          mk_heq(v, mk_let(n, Const("x"), val, body))),
                                      mk_refl_th(ty_v, v),
                                      pf);
+#endif
         return make_pair(new_v, proof);
     } else {
         throw rewriter_exception();
@@ -402,23 +317,26 @@ pair<expr, expr> rewrite_let_type(environment const & env, context & ctx, expr c
           rewritten term of val and \c pf_val the proof of (val = val')
    \return pair of v' = (let n : ty = val' in body), and proof of v = v'
 */
-pair<expr, expr> rewrite_let_value(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_value) {
+pair<expr, expr> rewrite_let_value(environment const & env, context & /* ctx */, expr const & v, pair<expr, expr> const & result_value) {
     lean_assert(is_let(v));
     type_inferer ti(env);
     name const & n       = let_name(v);
     optional<expr> const & ty = let_type(v);
-    expr const & val     = let_value(v);
+    // expr const & val     = let_value(v);
     expr const & body    = let_body(v);
     expr const & new_val = result_value.first;
-    expr const & pf      = result_value.second;
+    // expr const & pf      = result_value.second;
     expr const & new_v   = mk_let(n, ty, new_val, body);
-    expr const & ty_val  = ti(val, ctx);
+    // expr const & ty_val  = ti(val, ctx);
-    expr const & ty_v    = ti(v, ctx);
+    // expr const & ty_v    = ti(v, ctx);
+    expr proof;
+    #if 0 // TODO(Leo): HEq is gone
     expr const & proof   = mk_subst_th(ty_val, val, new_val,
                                  Fun({Const("x"), ty_val},
                                      mk_heq(v, mk_let(n, ty, Const("x"), body))),
                                  mk_refl_th(ty_v, v),
                                  pf);
+    #endif
     return make_pair(new_v, proof);
 }
 
@@ -435,23 +353,26 @@ pair<expr, expr> rewrite_let_value(environment const & env, context & ctx, expr
           body')
    \return pair of v' = (let n : ty = val in body'), and proof of v = v'
 */
-pair<expr, expr> rewrite_let_body(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_body) {
+pair<expr, expr> rewrite_let_body(environment const & env, context & /* ctx */, expr const & v, pair<expr, expr> const & result_body) {
     lean_assert(is_let(v));
     type_inferer ti(env);
     name const & n        = let_name(v);
     optional<expr> const & ty = let_type(v);
     expr const & val      = let_value(v);
-    expr const & body     = let_body(v);
+    // expr const & body     = let_body(v);
     expr const & new_body = result_body.first;
-    expr const & pf       = result_body.second;
+    // expr const & pf       = result_body.second;
     expr const & new_v    = mk_let(n, ty, val, new_body);
-    expr const & ty_body  = ti(body, extend(ctx, n, ty, body));
+    // expr const & ty_body  = ti(body, extend(ctx, n, ty, body));
-    expr const & ty_v     = ti(v, ctx);
+    // expr const & ty_v     = ti(v, ctx);
+    expr proof;
+#if 0 // TODO(Leo): HEq is gone
     expr const & proof    = mk_subst_th(ty_body, body, new_body,
                                   Fun({Const("e"), ty_body},
                                       mk_heq(v, mk_let(n, ty, val, Const("e")))),
                                   mk_refl_th(ty_v, v),
                                   pf);
+#endif
     return make_pair(new_v, proof);
 }
 
@@ -527,6 +448,7 @@ theorem_rewriter_cell::theorem_rewriter_cell(expr const & type, expr const & bod
         m_pattern = abst_body(m_pattern);
         m_num_args++;
     }
+#if 0 // HEq is gone
     if (!is_heq(m_pattern)) {
         lean_trace("rewriter", tout << "Theorem " << m_type << " is not in the form of "
                    << "Pi (x_1 : t_1 ... x_n : t_n), pattern = rhs" << endl;);
@@ -535,6 +457,7 @@ theorem_rewriter_cell::theorem_rewriter_cell(expr const & type, expr const & bod
     m_pattern = heq_lhs(m_pattern);
 
     lean_trace("rewriter", tout << "Number of Arg = " << m_num_args << endl;);
+#endif
 }
 theorem_rewriter_cell::~theorem_rewriter_cell() { }
 pair<expr, expr> theorem_rewriter_cell::operator()(environment const &, context &, expr const & v) const throw(rewriter_exception) {

src/library/rewriter/rewriter.h

@@ -43,9 +43,6 @@ std::pair<expr, expr> rewrite_lambda(environment const & env, context & ctx, exp
 std::pair<expr, expr> rewrite_pi_type(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_ty);
 std::pair<expr, expr> rewrite_pi_body(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_body);
 std::pair<expr, expr> rewrite_pi(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_ty, std::pair<expr, expr> const & result_body);
-std::pair<expr, expr> rewrite_eq_lhs(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_lhs);
-std::pair<expr, expr> rewrite_eq_rhs(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_rhs);
-std::pair<expr, expr> rewrite_eq(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_lhs, std::pair<expr, expr> const & result_rhs);
 std::pair<expr, expr> rewrite_let_type(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_ty);
 std::pair<expr, expr> rewrite_let_value(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_value);
 std::pair<expr, expr> rewrite_let_body(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_body);
@@ -387,37 +384,6 @@ class apply_rewriter_fn {
             }
         }
             break;
-        case expr_kind::HEq: {
-            expr const & lhs = heq_lhs(v);
-            expr const & rhs = heq_rhs(v);
-            std::pair<expr, expr> result_lhs = apply(env, ctx, lhs);
-            std::pair<expr, expr> result_rhs = apply(env, ctx, rhs);
-            expr const & new_lhs = result_lhs.first;
-            expr const & new_rhs = result_rhs.first;
-            if (lhs != new_lhs) {
-                if (rhs != new_rhs) {
-                    // lhs & rhs changed
-                    result = rewrite_eq(env, ctx, v, result_lhs, result_rhs);
-                } else {
-                    // only lhs changed
-                    result = rewrite_eq_lhs(env, ctx, v, result_lhs);
-                }
-            } else {
-                if (rhs != new_rhs) {
-                    // only rhs changed
-                    result = rewrite_eq_rhs(env, ctx, v, result_rhs);
-                } else {
-                    // nothing changed
-                    result = std::make_pair(v, mk_refl_th(ti(v, ctx), v));
-                }
-            }
-            std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
-            if (result.first != tmp.first) {
-                tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second);
-                result = tmp;
-            }
-        }
-            break;
         case expr_kind::Lambda: {
             name const & n = abst_name(v);
             expr const & ty = abst_domain(v);

src/library/simplifier/ceq.cpp

@@ -180,10 +180,6 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset,
         return
             is_permutation(abst_domain(lhs), abst_domain(rhs), offset, p) &&
             is_permutation(abst_body(lhs), abst_body(rhs), offset+1, p);
-    case expr_kind::HEq:
-        return
-            is_permutation(heq_lhs(lhs), heq_lhs(rhs), offset, p) &&
-            is_permutation(heq_rhs(lhs), heq_rhs(rhs), offset, p);
     case expr_kind::App:
         if (num_args(lhs) == num_args(rhs)) {
             for (unsigned i = 0; i < num_args(lhs); i++) {

src/tests/kernel/expr.cpp

@@ -76,8 +76,6 @@ static unsigned depth2(expr const & e) {
             std::accumulate(begin_args(e), end_args(e), 0,
                             [](unsigned m, expr const & arg){ return std::max(depth2(arg), m); })
             + 1;
-    case expr_kind::HEq:
-        return std::max(depth2(heq_lhs(e)), depth2(heq_rhs(e))) + 1;
     case expr_kind::Lambda: case expr_kind::Pi:
         return std::max(depth2(abst_domain(e)), depth2(abst_body(e))) + 1;
     case expr_kind::Let:
@@ -135,8 +133,6 @@ static unsigned count_core(expr const & a, expr_set & s) {
     case expr_kind::App:
         return std::accumulate(begin_args(a), end_args(a), 1,
                           [&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); });
-    case expr_kind::HEq:
-        return count_core(heq_lhs(a), s) + count_core(heq_rhs(a), s) + 1;
     case expr_kind::Lambda: case expr_kind::Pi:
         return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1;
     case expr_kind::Let:
@@ -295,7 +291,7 @@ static void tst13() {
 }
 
 static void tst14() {
-    expr t = HEq(Const("a"), Const("b"));
+    expr t = mk_eq(Const("A"), Const("a"), Const("b"));
     check_serializer(t);
     std::cout << t << "\n";
     expr l = mk_let("a", none_expr(), Const("b"), Var(0));
@@ -329,9 +325,6 @@ static void tst15() {
     lean_assert(has_metavar(f(a, a, m)));
     lean_assert(has_metavar(f(a, m, a, a)));
     lean_assert(!has_metavar(f(a, a, a, a)));
-    lean_assert(!has_metavar(HEq(a, f(a))));
-    lean_assert(has_metavar(HEq(m, f(a))));
-    lean_assert(has_metavar(HEq(a, f(m))));
 }
 
 static void check_copy(expr const & e) {
@@ -346,7 +339,6 @@ static void tst16() {
     expr a = Const("a");
     check_copy(iVal(10));
     check_copy(f(a));
-    check_copy(HEq(f(a), a));
     check_copy(mk_metavar("M"));
     check_copy(mk_lambda("x", a, Var(0)));
     check_copy(mk_pi("x", a, Var(0)));

src/tests/kernel/free_vars.cpp

@@ -75,11 +75,9 @@ static void tst4() {
     lean_assert(fn(Fun({x, Type()}, Var(0))) == 0);
     lean_assert(fn(Fun({x, Var(0)}, Var(0))) == 1);
     lean_assert(fn(Fun({x, Var(0)}, Var(2))) == 2);
-    lean_assert(fn(Fun({x, Var(0)}, HEq(Var(2), Var(1)))) == 2);
     lean_assert(fn(Pi({x, Type()}, Var(0))) == 0);
     lean_assert(fn(Pi({x, Var(0)}, Var(0))) == 1);
     lean_assert(fn(Pi({x, Var(0)}, Var(2))) == 2);
-    lean_assert(fn(Pi({x, Var(0)}, HEq(Var(2), Var(1)))) == 2);
     context ctx;
     ctx = extend(ctx, name("x"), Bool);
     ctx = extend(ctx, name("y"), Bool);

src/tests/kernel/metavar.cpp

@@ -275,7 +275,7 @@ static void tst14() {
     expr y = Const("y");
     env->add_var("h", Pi({N, Type()}, N >> (N >> N)));
     expr F1 = Fun({{N, Type()}, {a, N}, {f, N >> N}},
-                  (Fun({{x, N}, {y, N}}, HEq(f(m1), y)))(a));
+                  (Fun({{x, N}, {y, N}}, mk_eq(N, f(m1), y)))(a));
     metavar_env menv2 = menv.copy();
     menv2->assign(m1, h(Var(4), Var(1), Var(3)));
     normalizer norm(env);
@@ -287,12 +287,6 @@ static void tst14() {
     std::cout << norm(menv2->instantiate_metavars(F1)) << "\n";
     lean_assert(menv2->instantiate_metavars(norm(F1)) ==
                 norm(menv2->instantiate_metavars(F1)));
-    expr F2 = (Fun({{N, Type()}, {f, N >> N}, {a, N}, {b, N}},
-                   (Fun({{x, N}, {y, N}}, HEq(f(m1), y)))(a, m2)))(M);
-    std::cout << norm(F2) << "\n";
-    expr F3 = (Fun({{N, Type()}, {f, N >> N}, {a, N}, {b, N}},
-                   (Fun({{x, N}, {y, N}}, HEq(f(m1), y)))(b, m2)))(M);
-    std::cout << norm(F3) << "\n";
 }
 
 static void tst15() {

src/tests/kernel/normalizer.cpp

@@ -76,8 +76,6 @@ unsigned count_core(expr const & a, expr_set & s) {
     case expr_kind::App:
         return std::accumulate(begin_args(a), end_args(a), 1,
                                [&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); });
-    case expr_kind::HEq:
-        return count_core(heq_lhs(a), s) + count_core(heq_rhs(a), s) + 1;
     case expr_kind::Lambda: case expr_kind::Pi:
         return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1;
     case expr_kind::Let:
@@ -197,9 +195,9 @@ static void tst3() {
     env->add_var("a", Bool);
     expr t1 = Const("a");
     expr t2 = Const("a");
-    expr e = HEq(t1, t2);
+    expr e = mk_eq(Bool, t1, t2);
     std::cout << e << " --> " << normalize(e, env) << "\n";
-    lean_assert(normalize(e, env) == HEq(t1, t2));
+    lean_assert(normalize(e, env) == mk_eq(Bool, t1, t2));
 }
 
 static void tst4() {

src/tests/kernel/type_checker.cpp

@@ -80,7 +80,7 @@ static void tst2() {
 static void tst3() {
     environment env;
     init_test_frontend(env);
-    expr f = Fun("a", Bool, HEq(Const("a"), True));
+    expr f = Fun("a", Bool, mk_eq(Bool, Const("a"), True));
     std::cout << type_check(f, env) << "\n";
     lean_assert(type_check(f, env) == mk_arrow(Bool, Bool));
     expr t = mk_let("a", none_expr(), True, Var(0));
@@ -90,7 +90,7 @@ static void tst3() {
 static void tst4() {
     environment env;
     init_test_frontend(env);
-    expr a = HEq(iVal(1), iVal(2));
+    expr a = mk_eq(Int, iVal(1), iVal(2));
     expr pr   = mk_lambda("x", a, Var(0));
     std::cout << type_check(pr, env) << "\n";
 }
@@ -191,7 +191,7 @@ static void tst10() {
     expr t1 = Let({{a, f(b)}, {a, f(a)}}, f(a));
     expr t2 = f(f(f(b)));
     std::cout << t1 << " --> " << normalize(t1, env) << "\n";
-    expr prop  = HEq(t1, t2);
+    expr prop  = mk_eq(Int, t1, t2);
     expr proof = mk_refl_th(Int, t1);
     env->add_theorem("simp_eq", prop, proof);
     std::cout << env->get_object("simp_eq").get_name() << "\n";
@@ -215,8 +215,8 @@ static void tst11() {
         t3 = f(t3, t3);
     }
     lean_assert(t1 != t2);
-    env->add_theorem("eqs1", HEq(t1, t2), mk_refl_th(Int, t1));
+    env->add_theorem("eqs1", mk_eq(Int, t1, t2), mk_refl_th(Int, t1));
-    env->add_theorem("eqs2", HEq(t1, t3), mk_refl_th(Int, t1));
+    env->add_theorem("eqs2", mk_eq(Int, t1, t3), mk_refl_th(Int, t1));
 }
 
 static expr mk_big(unsigned depth) {
@@ -257,7 +257,7 @@ static void tst13() {
     env->add_var("f", Type() >> Type());
     expr f = Const("f");
     std::cout << type_check(f(Bool), env) << "\n";
-    std::cout << type_check(f(HEq(True, False)), env) << "\n";
+    std::cout << type_check(f(mk_eq(Bool, True, False)), env) << "\n";
 }
 
 static void tst14() {

src/tests/library/arith.cpp

@@ -110,10 +110,10 @@ static void tst5() {
     environment env;
     init_test_frontend(env);
     env->add_var(name("a"), Int);
-    expr e = HEq(iVal(3), iVal(4));
+    expr e = mk_eq(Int, iVal(3), iVal(4));
     std::cout << e << " --> " << normalize(e, env) << "\n";
     lean_assert(normalize(e, env) == False);
-    lean_assert(normalize(HEq(Const("a"), iVal(3)), env) == HEq(Const("a"), iVal(3)));
+    lean_assert(normalize(mk_eq(Int, Const("a"), iVal(3)), env) == mk_eq(Int, Const("a"), iVal(3)));
 }
 
 static void tst6() {

src/tests/library/deep_copy.cpp

@@ -18,7 +18,7 @@ static void tst1() {
     expr z = Const("z");
     local_context lctx{mk_lift(0, 1), mk_inst(0, a)};
     expr m = mk_metavar("a", lctx);
-    expr F = mk_let("z", Type(), Type(level()+1), mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), HEq(x, m)))));
+    expr F = mk_let("z", Type(), Type(level()+1), mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), f(x, m)))));
     expr G = deep_copy(F);
     lean_assert(F == G);
     lean_assert(!is_eqp(F, G));

src/tests/library/elaborator/elaborator.cpp

@@ -257,10 +257,10 @@ static void tst6() {
     env->add_var("f", Int >> (Int >> Int));
     env->add_var("a", Int);
     env->add_var("b", Int);
-    env->add_axiom("H1", HEq(f(a, f(a, b)), a));
+    env->add_axiom("H1", mk_eq(Int, f(a, f(a, b)), a));
-    env->add_axiom("H2", HEq(a, b));
+    env->add_axiom("H2", mk_eq(Int, a, b));
     expr V = mk_subst_th(m1, m2, m3, m4, H1, H2);
-    expr expected = HEq(f(a, f(b, b)), a);
+    expr expected = mk_eq(Int, f(a, f(b, b)), a);
     expr given    = checker.check(V, context(), menv, ucs);
     ucs.push_back(mk_eq_constraint(context(), expected, given, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
@@ -339,8 +339,8 @@ static void tst8() {
     env->add_var("a", Bool);
     env->add_var("b", Bool);
     env->add_var("c", Bool);
-    env->add_axiom("H1", HEq(a, b));
+    env->add_axiom("H1", mk_eq(Bool, a, b));
-    env->add_axiom("H2", HEq(b, c));
+    env->add_axiom("H2", mk_eq(Bool, b, c));
     success(mk_trans_th(_, _, _, _, H1, H2), mk_trans_th(Bool, a, b, c, H1, H2), env);
     success(mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1)),
             mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1)), env);
@@ -362,7 +362,11 @@ static void tst9() {
     env->add_var("vec", Nat >> Type());
     expr n   = Const("n");
     expr vec = Const("vec");
-    env->add_var("f", Pi({n, Nat}, vec(n) >> Nat));
+    std::cout << "step1\n";
+    expr z = Const("z");
+    env->add_var("z", Nat);
+    env->add_var("f", Pi({n, Nat}, vec(z) >> Nat));
+    std::cout << "step2\n";
     expr f = Const("f");
     expr a = Const("a");
     expr b = Const("b");
@@ -370,18 +374,18 @@ static void tst9() {
     expr fact = Const("fact");
     env->add_var("a", Nat);
     env->add_var("b", Nat);
-    env->add_definition("fact", Bool, HEq(a, b));
+    env->add_definition("fact", Bool, mk_eq(Nat, a, b));
     env->add_axiom("H", fact);
     success(mk_congr2_th(_, _, _, _, f, H),
-            mk_congr2_th(Nat, Fun({n, Nat}, vec(n) >> Nat), a, b, f, H), env);
+            mk_congr2_th(Nat, vec(z) >> Nat, a, b, f, H), env);
-    env->add_var("g", Pi({n, Nat}, vec(n) >> Nat));
+    env->add_var("g", Pi({n, Nat}, vec(z) >> Nat));
     expr g = Const("g");
-    env->add_axiom("H2", HEq(f, g));
+    env->add_axiom("H2", mk_eq(Pi({n, Nat}, vec(z) >> Nat), f, g));
     expr H2 = Const("H2");
     success(mk_congr_th(_, _, _, _, _, _, H2, H),
-            mk_congr_th(Nat, Fun({n, Nat}, vec(n) >> Nat), f, g, a, b, H2, H), env);
+            mk_congr_th(Nat, vec(z) >> Nat, f, g, a, b, H2, H), env);
     success(mk_congr_th(_, _, _, _, _, _, mk_refl_th(_, f), H),
-            mk_congr_th(Nat, Fun({n, Nat}, vec(n) >> Nat), f, f, a, b, mk_refl_th(Pi({n, Nat}, vec(n) >> Nat), f), H), env);
+            mk_congr_th(Nat, vec(z) >> Nat, f, f, a, b, mk_refl_th(Pi({n, Nat}, vec(z) >> Nat), f), H), env);
     success(mk_refl_th(_, a), mk_refl_th(Nat, a), env);
 }
 
@@ -402,11 +406,11 @@ static void tst10() {
     expr z   = Const("z");
     success(Fun({{x, _}, {y, _}}, f(x, y)),
             Fun({{x, Nat}, {y, R >> Nat}}, f(x, y)), env);
-    success(Fun({{x, _}, {y, _}, {z, _}}, HEq(f(x, y), f(x, z))),
+    success(Fun({{x, _}, {y, _}, {z, _}}, mk_eq(_, f(x, y), f(x, z))),
-            Fun({{x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, HEq(f(x, y), f(x, z))), env);
+            Fun({{x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, mk_eq(R, f(x, y), f(x, z))), env);
     expr A   = Const("A");
-    success(Fun({{A, Type()}, {x, _}, {y, _}, {z, _}}, HEq(f(x, y), f(x, z))),
+    success(Fun({{A, Type()}, {x, _}, {y, _}, {z, _}}, mk_eq(_, f(x, y), f(x, z))),
-            Fun({{A, Type()}, {x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, HEq(f(x, y), f(x, z))), env);
+            Fun({{A, Type()}, {x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, mk_eq(R, f(x, y), f(x, z))), env);
 }
 
 static void tst11() {
@@ -464,11 +468,11 @@ static void tst13() {
             Fun({{A, Type()}, {x, A}}, f(A, x)), env);
     success(Fun({{A, Type()}, {B, Type()}, {x, _}}, f(A, x)),
             Fun({{A, Type()}, {B, Type()}, {x, A}}, f(A, x)), env);
-    success(Fun({{A, Type()}, {B, Type()}, {x, _}}, HEq(f(B, x), f(_, x))),
+    success(Fun({{A, Type()}, {B, Type()}, {x, _}}, mk_eq(_, f(B, x), f(_, x))),
-            Fun({{A, Type()}, {B, Type()}, {x, B}}, HEq(f(B, x), f(B, x))), env);
+            Fun({{A, Type()}, {B, Type()}, {x, B}}, mk_eq(B, f(B, x), f(B, x))), env);
-    success(Fun({{A, Type()}, {B, Type()}, {x, _}}, HEq(f(B, x), f(_, x))),
+    success(Fun({{A, Type()}, {B, Type()}, {x, _}}, mk_eq(B, f(B, x), f(_, x))),
-            Fun({{A, Type()}, {B, Type()}, {x, B}}, HEq(f(B, x), f(B, x))), env);
+            Fun({{A, Type()}, {B, Type()}, {x, B}}, mk_eq(B, f(B, x), f(B, x))), env);
-    unsolved(Fun({{A, _}, {B, _}, {x, _}}, HEq(f(B, x), f(_, x))), env);
+    unsolved(Fun({{A, _}, {B, _}, {x, _}}, mk_eq(_, f(B, x), f(_, x))), env);
 }
 
 static void tst14() {
@@ -493,23 +497,6 @@ static void tst14() {
     success(Fun({g, Pi({A, TypeU}, A >> (A >> Bool))}, g(_, Bool, N)),
             Fun({g, Pi({A, TypeU}, A >> (A >> Bool))}, g(Type(), Bool, N)),
             env);
-    success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
-                g(_,
-                  Fun({{x, _}, {y, _}}, HEq(f(_, x), f(_, y))),
-                  Fun({{x, N}, {y, Bool}}, True))),
-            Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
-                g((N >> (Bool >> Bool)),
-                  Fun({{x, N}, {y, Bool}}, HEq(f(N, x), f(Bool, y))),
-                  Fun({{x, N}, {y, Bool}}, True))), env);
-
-    success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
-                g(_,
-                  Fun({{x, N}, {y, _}}, HEq(f(_, x), f(_, y))),
-                  Fun({{x, _}, {y, Bool}}, True))),
-            Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
-                g((N >> (Bool >> Bool)),
-                  Fun({{x, N}, {y, Bool}}, HEq(f(N, x), f(Bool, y))),
-                  Fun({{x, N}, {y, Bool}}, True))), env);
 }
 
 static void tst15() {
@@ -550,28 +537,28 @@ static void tst16() {
     env->add_var("a", Bool);
     env->add_var("b", Bool);
     env->add_var("c", Bool);
-    success(Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}},
+    success(Fun({{H1, mk_eq(_, a, b)}, {H2, mk_eq(_, b, c)}},
                 mk_trans_th(_, _, _, _, H1, H2)),
-            Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}},
+            Fun({{H1, mk_eq(Bool, a, b)}, {H2, mk_eq(Bool, b, c)}},
                 mk_trans_th(Bool, a, b, c, H1, H2)),
             env);
     expr H3 = Const("H3");
-    success(Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}},
+    success(Fun({{H1, mk_eq(Bool, a, b)}, {H2, mk_eq(Bool, b, c)}, {H3, a}},
                 mk_eqt_intro_th(_, mk_eqmp_th(_, _, mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), H3))),
-            Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}},
+            Fun({{H1, mk_eq(Bool, a, b)}, {H2, mk_eq(Bool, b, c)}, {H3, a}},
                 mk_eqt_intro_th(c, mk_eqmp_th(a, c, mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), H3))),
             env);
     environment env2;
     init_test_frontend(env2);
-    success(Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}},
+    success(Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, mk_eq(_, a, b)}, {H2, mk_eq(_, b, c)}, {H3, a}},
                 mk_eqt_intro_th(_, mk_eqmp_th(_, _, mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), H3))),
-            Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}},
+            Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, mk_eq(Bool, a, b)}, {H2, mk_eq(Bool, b, c)}, {H3, a}},
                 mk_eqt_intro_th(c, mk_eqmp_th(a, c, mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), H3))),
             env2);
     expr A = Const("A");
-    success(Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, HEq(a, b)}, {H2, HEq(b, c)}},
+    success(Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, mk_eq(_, a, b)}, {H2, mk_eq(_, b, c)}},
                 mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1)))),
-            Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, HEq(a, b)}, {H2, HEq(b, c)}},
+            Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, mk_eq(A, a, b)}, {H2, mk_eq(A, b, c)}},
                 mk_symm_th(A, c, a, mk_trans_th(A, c, b, a, mk_symm_th(A, b, c, H2), mk_symm_th(A, a, b, H1)))),
             env2);
 }
@@ -682,7 +669,7 @@ void tst21() {
     expr b  = Const("b");
     expr m1 = menv->mk_metavar();
     expr l = m1(b, a);
-    expr r = Fun({x, N}, f(x, HEq(a, b)));
+    expr r = Fun({x, N}, f(x, mk_eq(_, a, b)));
     elaborator elb(env, menv, context(), l, r);
     while (true) {
         try {
@@ -745,8 +732,8 @@ void tst23() {
     expr f  = Const("f");
     expr m1 = menv->mk_metavar();
     expr m2 = menv->mk_metavar();
-    expr l  = Fun({{x, N}, {y, N}}, HEq(y, f(x, m1)));
+    expr l  = Fun({{x, N}, {y, N}}, mk_eq(_, y, f(x, m1)));
-    expr r  = Fun({{x, N}, {y, N}}, HEq(m2, f(m1, x)));
+    expr r  = Fun({{x, N}, {y, N}}, mk_eq(_, m2, f(m1, x)));
     elaborator elb(env, menv, context(), l, r);
     while (true) {
         try {
@@ -832,13 +819,14 @@ void tst26() {
     expr a = Const("a");
     env->add_var("a", Type(level()+1));
     expr m1 = menv->mk_metavar();
-    expr F  = HEq(g(m1, a), a);
+    expr m2 = menv->mk_metavar();
+    expr F  = mk_eq(m2, g(m1, a), a);
     std::cout << F << "\n";
     std::cout << checker.check(F, context(), menv, ucs) << "\n";
     elaborator elb(env, menv, ucs.size(), ucs.data());
     metavar_env s = elb.next();
     std::cout << s->instantiate_metavars(F) << "\n";
-    lean_assert_eq(s->instantiate_metavars(F), HEq(g(Type(level()+1), a), a));
+    lean_assert_eq(s->instantiate_metavars(F), mk_eq(Type(level()+1), g(Type(level()+1), a), a));
 }
 
 void tst27() {

src/tests/library/expr_lt.cpp

@@ -34,10 +34,6 @@ static void tst1() {
     lt(Const("a"), Const("b"), true);
     lt(Const("a"), Const("a"), false);
     lt(Var(1), Const("a"), true);
-    lt(HEq(Var(0), Var(1)), HEq(Var(1), Var(1)), true);
-    lt(HEq(Var(1), Var(0)), HEq(Var(1), Var(1)), true);
-    lt(HEq(Var(1), Var(1)), HEq(Var(1), Var(1)), false);
-    lt(HEq(Var(2), Var(1)), HEq(Var(1), Var(1)), false);
     lt(Const("f")(Var(0)), Const("f")(Var(0), Const("a")), true);
     lt(Const("f")(Var(0), Const("a"), Const("b")), Const("f")(Var(0), Const("a")), false);
     lt(Const("f")(Var(0), Const("a")), Const("g")(Var(0), Const("a")), true);

src/tests/library/formatter.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/abstract.h"
 #include "kernel/formatter.h"
+#include "kernel/kernel.h"
 #include "library/printer.h"
 using namespace lean;
 
@@ -30,16 +31,12 @@ static void tst1() {
     expr x  = Const("x");
     expr y  = Const("y");
     expr N  = Const("N");
-    expr F  = Fun({x, Pi({x, N}, x >> x)}, Let({y, f(a)}, f(HEq(x, f(y, a)))));
-    check(fmt(F), "fun x : (Pi x : N, (x#0 -> x#1)), (let y := f a in (f (x#1 == (f y#0 a))))");
     check(fmt(env->get_object("N")), "variable N : Type");
     context ctx;
     ctx = extend(ctx, "x", f(a));
     ctx = extend(ctx, "y", f(Var(0), N >> N));
-    ctx = extend(ctx, "z", N, HEq(Var(0), Var(1)));
+    check(fmt(ctx, f(Var(0), Var(2))), "f y#0 #2");
-    check(fmt(ctx), "[x : f a; y : f x#0 (N -> N); z : N := y#0 == x#1]");
+    check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x#0 (N -> N)] |- f y#0 #2");
-    check(fmt(ctx, f(Var(0), Var(2))), "f z#0 x#2");
-    check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x#0 (N -> N); z : N := y#0 == x#1] |- f z#0 x#2");
 }
 
 int main() {

src/tests/library/max_sharing.cpp

@@ -15,14 +15,11 @@ static void tst1() {
     max_sharing_fn max_fn;
     expr a1 = Const("a");
     expr a2 = Const("a");
-    expr F1 = HEq(a1, a2);
-    lean_assert(!is_eqp(heq_lhs(F1), heq_rhs(F1)));
-    expr F2 = max_fn(F1);
-    lean_assert(is_eqp(heq_lhs(F2), heq_rhs(F2)));
     expr x = Const("x");
     expr y = Const("y");
     expr f = Const("f");
     expr N = Const("N");
+    expr F1, F2;
     F1 = f(Fun({x, N}, f(x, x)), Fun({y, N}, f(y, y)));
     lean_assert(!is_eqp(arg(F1, 1), arg(F1, 2)));
     F2 = max_fn(F1);

src/tests/library/rewriter/fo_match.cpp

@@ -273,7 +273,7 @@ static void match_let_tst1() {
 
 static void match_let_tst2() {
     cout << "--- match_let_tst2() ---" << endl;
-    expr t = HEq(Const("a"), Const("b"));
+    expr t = mk_eq(Const("A"), Const("a"), Const("b"));
     expr l = mk_let("a", Type(), Const("b"), Var(0));
     subst_map s;
     bool result = test_match(l, t, 0, s);
@@ -283,7 +283,7 @@ static void match_let_tst2() {
 
 static void match_let_tst3() {
     cout << "--- match_let_tst3() ---" << endl;
-    expr t = HEq(Const("a"), Const("b"));
+    expr t = mk_eq(Const("A"), Const("a"), Const("b"));
     expr l1 = mk_let("a", Var(0), Const("b"), Var(0));
     expr l2 = mk_let("a", Int, Const("b"), Var(0));
     subst_map s;
@@ -295,7 +295,7 @@ static void match_let_tst3() {
 
 static void match_let_tst4() {
     cout << "--- match_let_tst4() ---" << endl;
-    expr t = HEq(Const("a"), Const("b"));
+    expr t = mk_eq(Const("A"), Const("a"), Const("b"));
     expr l1 = mk_let("a", Nat, Const("b"), Var(0));
     expr l2 = mk_let("a", Int, Const("b"), Var(0));
     subst_map s;
@@ -306,7 +306,7 @@ static void match_let_tst4() {
 
 static void match_let_tst5() {
     cout << "--- match_let_tst5() ---" << endl;
-    expr t = HEq(Const("a"), Const("b"));
+    expr t = mk_eq(Const("A"), Const("a"), Const("b"));
     expr l1 = mk_let("a", Int, Var(3), Var(0));
     expr l2 = mk_let("a", Int, Const("b"), Const("b"));
     subst_map s;
@@ -317,7 +317,7 @@ static void match_let_tst5() {
 
 static void match_let_tst6() {
     cout << "--- match_let_tst6() ---" << endl;
-    expr t = HEq(Const("a"), Const("b"));
+    expr t = mk_eq(Const("A"), Const("a"), Const("b"));
     expr l1 = mk_let("a", Var(0), Var(1), Var(0));
     expr l2 = mk_let("a", Int, Const("b"), Const("b"));
     subst_map s;
@@ -328,7 +328,7 @@ static void match_let_tst6() {
 
 static void match_let_tst7() {
     cout << "--- match_let_tst7() ---" << endl;
-    expr t = HEq(Const("a"), Const("b"));
+    expr t = mk_eq(Const("A"), Const("a"), Const("b"));
     expr l1 = mk_let("a", Var(0), Var(1), Var(0));
     expr l2 = mk_let("a", Int, Const("b"), Var(0));
     subst_map s;
@@ -341,7 +341,7 @@ static void match_let_tst7() {
 
 static void match_let_tst8() {
     cout << "--- match_let_tst8() ---" << endl;
-    expr t = HEq(Const("a"), Const("b"));
+    expr t = mk_eq(Const("A"), Const("a"), Const("b"));
     expr l1 = mk_let("a", Nat, Var(1), Var(0));
     expr l2 = mk_let("a", Int, Const("b"), Var(0));
     subst_map s;
@@ -352,7 +352,7 @@ static void match_let_tst8() {
 
 static void match_let_tst9() {
     cout << "--- match_let_tst9() ---" << endl;
-    expr t = HEq(Const("a"), Const("b"));
+    expr t = mk_eq(Const("A"), Const("a"), Const("b"));
     expr l1 = mk_let("a", Var(0), Var(0), Var(0));
     expr l2 = mk_let("a", Nat, Const("b"), Const("a"));
     subst_map s;
@@ -367,7 +367,7 @@ static void match_eq_tst1() {
     expr f = Const("f");
     expr a = Const("a");
     subst_map s;
-    bool result = test_match(mk_heq(x, a), mk_heq(f, a), 0, s);
+    bool result = test_match(mk_eq(Const("A"), x, a), mk_eq(Const("A"), f, a), 0, s);
     lean_assert_eq(result, true);
     lean_assert_eq(s.find(0)->second, f);
     lean_assert_eq(s.size(), 1);
@@ -379,7 +379,7 @@ static void match_eq_tst2() {
     expr f = Const("f");
     expr a = Const("a");
     subst_map s;
-    bool result = test_match(mk_heq(mk_Nat_add(x, a), x), mk_heq(mk_Nat_add(f, a), f), 0, s);
+    bool result = test_match(mk_eq(Nat, mk_Nat_add(x, a), x), mk_eq(Nat, mk_Nat_add(f, a), f), 0, s);
     lean_assert_eq(result, true);
     lean_assert_eq(s.find(0)->second, f);
     lean_assert_eq(s.size(), 1);
@@ -391,7 +391,7 @@ static void match_eq_tst3() {
     expr f = Const("f");
     expr a = Const("a");
     subst_map s;
-    bool result = test_match(mk_heq(mk_Nat_add(x, a), x), f, 0, s);
+    bool result = test_match(mk_eq(Nat, mk_Nat_add(x, a), x), f, 0, s);
     lean_assert_eq(result, false);
     lean_assert_eq(s.empty(), true);
 }

src/tests/library/rewriter/rewriter.cpp

@@ -21,6 +21,9 @@ Author: Soonho Kong
 #include "frontends/lean/frontend.h"
 using namespace lean;
 
+#if 0
+// TODO(Leo): migrate to homogeneous equality
+
 using std::cout;
 using std::pair;
 using lean::endl;
@@ -54,7 +57,7 @@ static void theorem_rewriter1_tst() {
     cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << std::endl;
     cout << "         " << concl << " := " << proof << std::endl;
 
-    lean_assert_eq(concl, mk_heq(a_plus_b, b_plus_a));
+    lean_assert_eq(concl, mk_eq(Nat, a_plus_b, b_plus_a));
     lean_assert_eq(proof, Const("ADD_COMM")(a, b));
     env->add_theorem("New_theorem1", concl, proof);
 }
@@ -749,3 +752,9 @@ int main() {
     lambda_type_rewriter_tst();
     return has_violations() ? 1 : 0;
 }
+#else
+int main() {
+    save_stack_info();
+    return has_violations() ? 1 : 0;
+}
+#endif

src/tests/library/update_expr.cpp

@@ -12,12 +12,6 @@ using namespace lean;
 static void tst1() {
     expr a = Const("a");
     expr b = Const("b");
-    expr eq1 = HEq(a, b);
-    expr eq2 = update_heq(eq1, a, a);
-    expr eq3 = update_heq(eq1, a, b);
-    lean_assert(heq_lhs(eq3) == a);
-    lean_assert(heq_rhs(eq3) == b);
-    lean_assert(is_eqp(eq1, eq3));
 }
 
 static void tst2() {

tests/lean/abst.lean

@@ -1,5 +1,5 @@
 import Int.
-axiom PlusComm(a b : Int) : a + b == b + a.
+axiom PlusComm(a b : Int) : a + b = b + a.
 variable a : Int.
 check (funext (fun x : Int, (PlusComm a x))).
 set_option pp::implicit true.

tests/lean/abst.lean.expected.out

@@ -3,7 +3,7 @@
   Imported 'Int'
   Assumed: PlusComm
   Assumed: a
-funext (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a)
+funext (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) = (λ x : ℤ, x + a)
   Set: lean::pp::implicit
 @funext ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) :
-    (λ x : ℤ, a + x) == (λ x : ℤ, x + a)
+    @eq (∀ x : ℤ, (λ x : ℤ, ℤ) x) (λ x : ℤ, a + x) (λ x : ℤ, x + a)

tests/lean/arith6.lean.expected.out

@@ -8,8 +8,8 @@ false
 true
 true
   Assumed: x
-3 + -1 * (x * (3 div x)) == 0
+3 + -1 * (x * (3 div x)) = 0
-x + -1 * (3 * (x div 3)) == 0
+x + -1 * (3 * (x div 3)) = 0
 false
   Set: lean::pp::notation
 Int::divides 3 x

tests/lean/bad10.lean

@@ -2,7 +2,7 @@ set_option pp::implicit true.
 set_option pp::colors   false.
 variable N : Type.
 
-definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ :=
+definition T (a : N) (f : _ -> _) (H : f a = a) : f (f _) = f _ :=
-substp (fun x : N, f (f a) == _) (refl (f (f _))) H.
+substp (fun x : N, f (f a) = _) (refl (f (f _))) H.
 
 print environment 1.

tests/lean/bad10.lean.expected.out

@@ -4,5 +4,5 @@
   Set: pp::colors
   Assumed: N
   Defined: T
-definition T (a : N) (f : N → N) (H : f a == a) : f (f a) == f (f a) :=
+definition T (a : N) (f : N → N) (H : @eq N (f a) a) : @eq N (f (f a)) (f (f a)) :=
-    @substp N (f a) a (λ x : N, f (f a) == f (f a)) (@refl N (f (f a))) H
+    @substp N (f a) a (λ x : N, @eq N (f (f a)) (f (f a))) (@refl N (f (f a))) H

tests/lean/bad9.lean

@@ -3,6 +3,6 @@ set_option pp::colors   false.
 variable N : Type.
 
 check
-fun (a : N) (f : N -> N) (H : f a == a),
+fun (a : N) (f : N -> N) (H : f a = a),
-let calc1 : f a == a := substp (fun x : N, f a == _) (refl (f a)) H
+let calc1 : f a = a := substp (fun x : N, f a = _) (refl (f a)) H
 in  calc1.

tests/lean/bad9.lean.expected.out

@@ -3,6 +3,6 @@
   Set: lean::pp::implicit
   Set: pp::colors
   Assumed: N
-λ (a : N) (f : N → N) (H : f a == a),
+λ (a : N) (f : N → N) (H : @eq N (f a) a),
-  let calc1 : f a == a := @substp N (f a) a (λ x : N, f a == x) (@refl N (f a)) H in calc1 :
+  let calc1 : @eq N (f a) a := @substp N (f a) a (λ x : N, @eq N (f a) x) (@refl N (f a)) H in calc1 :
-    ∀ (a : N) (f : N → N), f a == a → f a == a
+    ∀ (a : N) (f : N → N), @eq N (f a) a → @eq N (f a) a

tests/lean/bug.lean

@@ -1 +1 @@
-check fun (A A' : (Type U)) (H : A == A'), symm H
+check fun (A A' : (Type U')) (H : A = A'), symm H

tests/lean/bug.lean.expected.out

@@ -1,11 +1,10 @@
   Set: pp::colors
   Set: pp::unicode
 Failed to solve
-A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≺ TypeU
+A : (Type U'), A' : (Type U') ⊢ ?M::4 ≺ (Type U')
-    bug.lean:1:44: Type of argument 1 must be convertible to the expected type in the application of
+    bug.lean:1:37: Type of argument 1 must be convertible to the expected type in the application of
-        @symm
+        @eq
     with arguments:
         ?M::0
         A
         A'
-        H

tests/lean/cast1.lean

@@ -1,19 +0,0 @@
-import cast.
-import Int.
-
-variable vector : Type -> Nat -> Type
-axiom N0 (n : Nat) : n + 0 = n
-theorem V0 (T : Type) (n : Nat) : (vector T (n + 0)) = (vector T n) :=
-   congr (refl (vector T)) (N0 n)
-variable f (n : Nat) (v : vector Int n) : Int
-variable m : Nat
-variable v1 : vector Int (m + 0)
--- The following application will fail because (vector Int (m + 0)) and (vector Int m)
--- are not definitionally equal.
-check f m v1
--- The next one succeeds using the "casting" operator.
--- We can do it, because (V0 Int m) is a proof that
--- (vector Int (m + 0)) and (vector Int m) are propositionally equal.
--- That is, they have the same interpretation in the lean set theoretic
--- semantics.
-check f m (cast (V0 Int m) v1)

tests/lean/cast1.lean.expected.out

@@ -1,18 +0,0 @@
-  Set: pp::colors
-  Set: pp::unicode
-  Imported 'cast'
-  Imported 'Int'
-  Assumed: vector
-  Assumed: N0
-  Proved: V0
-  Assumed: f
-  Assumed: m
-  Assumed: v1
-cast1.lean:13:7: error: type mismatch at application
-    f m v1
-Function type:
-    ∀ (n : ℕ), vector ℤ n → ℤ
-Arguments types:
-    m : ℕ
-    v1 : vector ℤ (m + 0)
-f m (cast (V0 ℤ m) v1) : ℤ

tests/lean/cast2.lean

@@ -1,7 +0,0 @@
-import cast
-variable A : Type
-variable B : Type
-variable A' : Type
-variable B' : Type
-axiom H : (A -> B) = (A' -> B')
-variable a : A

tests/lean/cast2.lean.expected.out

@@ -1,9 +0,0 @@
-  Set: pp::colors
-  Set: pp::unicode
-  Imported 'cast'
-  Assumed: A
-  Assumed: B
-  Assumed: A'
-  Assumed: B'
-  Assumed: H
-  Assumed: a

tests/lean/cast3.lean

@@ -1,24 +0,0 @@
-import cast
-
-variables A A' B B' : Type
-variable x : A
-eval cast (refl A) x
-eval x = (cast (refl A) x)
-variable b : B
-definition f (x : A) : B := b
-axiom H : (A -> B) = (A' -> B)
-variable a' : A'
-eval (cast H f) a'
-axiom H2 : (A -> B) = (A' -> B')
-definition g (x : B') : Nat := 0
-eval g ((cast H2 f) a')
-check g ((cast H2 f) a')
-
-eval (cast H2 f) a'
-
-variables A1 A2 A3 : Type
-axiom Ha : A1 = A2
-axiom Hb : A2 = A3
-variable a : A1
-eval (cast Hb (cast Ha a))
-check (cast Hb (cast Ha a))

tests/lean/cast3.lean.expected.out

@@ -1,28 +0,0 @@
-  Set: pp::colors
-  Set: pp::unicode
-  Imported 'cast'
-  Assumed: A
-  Assumed: A'
-  Assumed: B
-  Assumed: B'
-  Assumed: x
-cast (refl A) x
-x == cast (refl A) x
-  Assumed: b
-  Defined: f
-  Assumed: H
-  Assumed: a'
-cast H (λ x : A, b) a'
-  Assumed: H2
-  Defined: g
-0
-g (cast H2 f a') : ℕ
-cast H2 (λ x : A, b) a'
-  Assumed: A1
-  Assumed: A2
-  Assumed: A3
-  Assumed: Ha
-  Assumed: Hb
-  Assumed: a
-cast Hb (cast Ha a)
-cast Hb (cast Ha a) : A3

tests/lean/cast4.lean

@@ -1,13 +0,0 @@
-import cast
-set_option pp::colors false
-
-check fun (A A': TypeM)
-          (B   : A -> TypeM)
-          (B'  : A' -> TypeM)
-          (f   : forall x : A, B x)
-          (g   : forall x : A', B' x)
-          (a   : A)
-          (b   : A')
-          (H2  : f == g)
-          (H3  : a == b),
-     hcongr H2 H3

tests/lean/cast4.lean.expected.out

@@ -1,22 +0,0 @@
-  Set: pp::colors
-  Set: pp::unicode
-  Imported 'cast'
-  Set: pp::colors
-λ (A A' : TypeM)
-  (B : A → TypeM)
-  (B' : A' → TypeM)
-  (f : ∀ x : A, B x)
-  (g : ∀ x : A', B' x)
-  (a : A)
-  (b : A')
-  (H2 : f == g)
-  (H3 : a == b),
-  hcongr H2 H3 :
-    ∀ (A A' : TypeM)
-      (B : A → TypeM)
-      (B' : A' → TypeM)
-      (f : ∀ x : A, B x)
-      (g : ∀ x : A', B' x)
-      (a : A)
-      (b : A'),
-      f == g → a == b → f a == g b

tests/lean/elab7.lean

@@ -2,7 +2,7 @@ variables A B C : (Type U)
 variable P : A -> Bool
 variable F1 : A -> B -> C
 variable F2 : A -> B -> C
-variable H : forall (a : A) (b : B), (F1 a b) == (F2 a b)
+variable H : forall (a : A) (b : B), (F1 a b) = (F2 a b)
 variable a : A
 check eta (F2 a)
 check funext (fun a : A,

tests/lean/elab7.lean.expected.out

@@ -9,9 +9,8 @@
   Assumed: H
   Assumed: a
 eta (F2 a) : (λ x : B, F2 a x) = F2 a
-funext (λ a : A, symm (eta (F1 a)) ⋈ (funext (λ b : B, H a b) ⋈ eta (F2 a))) :
+funext (λ a : A, symm (eta (F1 a)) ⋈ (funext (λ b : B, H a b) ⋈ eta (F2 a))) : (λ x : A, F1 x) = (λ x : A, F2 x)
-    (λ x : A, F1 x) == (λ x : A, F2 x)
+funext (λ a : A, funext (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) = (λ (x : A) (x::1 : B), F2 x x::1)
-funext (λ a : A, funext (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) == (λ (x : A) (x::1 : B), F2 x x::1)
   Proved: T1
   Proved: T2
   Proved: T3

tests/lean/eq3.lean

@@ -1,11 +1,8 @@
-import cast
 variable Vector : Nat -> Type
 variable n  : Nat
 variable v1 : Vector n
 variable v2 : Vector (n + 0)
 variable v3 : Vector (0 + n)
-axiom H1 : v1 == v2
+axiom cast {A B : TypeU} : A = B -> A -> B
-axiom H2 : v2 == v3
+axiom H1 : v1 = cast (congr2 Vector (Nat::add_zeror n)) v2
-check htrans H1 H2
+axiom H2 : v2 = cast (congr2 Vector (Nat::add_comm 0 n)) v3
-set_option pp::implicit true
-check htrans H1 H2

tests/lean/eq3.lean.expected.out

@@ -1,13 +1,10 @@
   Set: pp::colors
   Set: pp::unicode
-  Imported 'cast'
   Assumed: Vector
   Assumed: n
   Assumed: v1
   Assumed: v2
   Assumed: v3
+  Assumed: cast
   Assumed: H1
   Assumed: H2
-htrans H1 H2 : v1 == v3
-  Set: lean::pp::implicit
-@htrans (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3

tests/lean/eq4.lean

@@ -1,8 +1,4 @@
 import Int
-eval 1 == true
+import Real
-eval 1 == 1.0
+eval 1 = 1.0
-eval 1 == nat_to_int 1
+eval 1 = nat_to_int 1
-eval true == 1.0
-eval Nat::add == 1
-eval Nat::add == Nat::mul
-eval Int::add == Int::mul

tests/lean/eq4.lean.expected.out

@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
   Imported 'Int'
-1 == ⊤
+  Imported 'Real'
-1 == 1
+⊤
-1 == 1
+⊤
-⊤ == 1
-Nat::add == 1
-Nat::add == Nat::mul
-Int::add == Int::mul

tests/lean/find.lean.expected.out

@@ -1,8 +1,8 @@
   Set: pp::colors
   Set: pp::unicode
   Imported 'find'
-theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a
+theorem congr1 {A : TypeU'} {B : A → TypeU'} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a
-theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : ∀ x : A, B x) (H : a = b) : f a == f b
+theorem congr2 {A B : TypeU'} {a b : A} (f : A → B) (H : a = b) : f a = f b
-theorem congr {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} {a b : A} (H1 : f = g) (H2 : a = b) : f a == g b
+theorem congr {A B : TypeU'} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
 find.lean:3:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:24), no object name in the environment matches the regular expression 'foo'
 find.lean:4:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:18), unfinished capture

tests/lean/mod1.lean

@@ -1,11 +1,11 @@
-import cast
+import specialfn
-import cast
+import specialfn
 (*
    local env = environment() -- create new environment
    parse_lean_cmds([[
-      import cast
+      import specialfn
-      import cast
+      import specialfn
-      check @cast
+      check sin
    ]], env)
 *)
-check @cast
+check sin

tests/lean/mod1.lean.expected.out

@@ -1,6 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Imported 'cast'
+  Imported 'specialfn'
-  Imported 'cast'
+  Imported 'specialfn'
-@cast : ∀ (A B : TypeU), A == B → A → B
+sin : ℝ → ℝ
-@cast : ∀ (A B : TypeU), A == B → A → B
+sin : ℝ → ℝ

tests/lean/norm1.lean

@@ -7,7 +7,7 @@ variable H : (N -> N -> N) -> N
 eval fun f : N -> N, (fun x y : N, g x) (f a)
 eval fun (a : N) (f : N -> N) (g : (N -> N) -> N -> N) (h : N -> N -> N),
      (fun (x : N) (y : N) (z : N), h x y) (g (fun x : N, f (f x)) (f a)) (f a)
-eval fun (a b : N) (g : Bool -> N), (fun x y : Bool, g x) (a == b)
+eval fun (a b : N) (g : Bool -> N), (fun x y : Bool, g x) (a = b)
 eval fun (a : Type) (b : a -> Type) (g : (Type U) -> Bool), (fun x y : (Type U), g x) (forall x : a, b x)
 eval fun f : N -> N, (fun x y z : N, g x) (f a)
 eval fun f g : N -> N, (fun x y z : N, g x) (f a)

tests/lean/norm1.lean.expected.out

@@ -7,7 +7,7 @@
   Assumed: H
 λ (f : N → N) (y : N), g (f a)
 λ (a : N) (f : N → N) (g : (N → N) → N → N) (h : N → N → N) (z : N), h (g (λ x : N, f (f x)) (f a)) (f a)
-λ (a b : N) (g : Bool → N) (y : Bool), g (a == b)
+λ (a b : N) (g : Bool → N) (y : Bool), g (a = b)
 λ (a : Type) (b : a → Type) (g : (Type U) → Bool) (y : (Type U)), g (∀ x : a, b x)
 λ (f : N → N) (y z : N), g (f a)
 λ (f g : N → N) (y z : N), g (f a)

tests/lean/norm_bug1.lean

@@ -1,27 +0,0 @@
-import cast
-set_option pp::colors false
-
-check fun (A A': TypeM)
-          (a   : A)
-          (b   : A')
-          (L2  : A' == A),
-   let b' : A        := cast     L2 b,
-       L3 : b == b'  := cast_eq L2 b
-   in L3
-
-check fun (A A': TypeM)
-          (B   : A -> TypeM)
-          (B'  : A' -> TypeM)
-          (f   : forall x : A, B x)
-          (g   : forall x : A', B' x)
-          (a   : A)
-          (b   : A')
-          (H2  : f == g)
-          (H3  : a == b),
-    let L1 : A  == A'               := type_eq H3,
-        L2 : A' == A                := symm L1,
-        b' : A                      := cast L2 b,
-        L3 : b  == b'               := cast_eq L2 b,
-        L4 : a == b'                := htrans H3 L3,
-        L5 : f a == f b'            := congr2 f L4
-    in L5

tests/lean/norm_bug1.lean.expected.out

@@ -1,32 +0,0 @@
-  Set: pp::colors
-  Set: pp::unicode
-  Imported 'cast'
-  Set: pp::colors
-λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast_eq L2 b in L3 :
-    ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
-λ (A A' : TypeM)
-  (B : A → TypeM)
-  (B' : A' → TypeM)
-  (f : ∀ x : A, B x)
-  (g : ∀ x : A', B' x)
-  (a : A)
-  (b : A')
-  (H2 : f == g)
-  (H3 : a == b),
-  let L1 : A == A' := type_eq H3,
-      L2 : A' == A := symm L1,
-      b' : A := cast L2 b,
-      L3 : b == b' := cast_eq L2 b,
-      L4 : a == b' := htrans H3 L3,
-      L5 : f a == f b' := congr2 f L4
-  in L5 :
-    ∀ (A A' : TypeM)
-      (B : A → TypeM)
-      (B' : A' → TypeM)
-      (f : ∀ x : A, B x)
-      (g : ∀ x : A', B' x)
-      (a : A)
-      (b : A')
-      (H2 : f == g)
-      (H3 : a == b),
-      f a == f (cast (symm (type_eq H3)) b)

tests/lean/tst1.lean.expected.out

@@ -26,7 +26,7 @@ definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A :=
 definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
     λ (i : N) (H : i < n), f (v1 i H) (v2 i H)
 select (update (const three ⊥) two ⊤) two two_lt_three : Bool
-if (two == two) then ⊤ else ⊥
+if (two = two) then ⊤ else ⊥
 update (const three ⊥) two ⊤ : vector Bool three
 
 --------
@@ -46,4 +46,4 @@ map normal form -->
   f (v1 i H) (v2 i H)
 
 update normal form --> 
-λ (A : Type) (n : N) (v : ∀ (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n), if (j == i) then d else v j H
+λ (A : Type) (n : N) (v : ∀ (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n), if (j = i) then d else v j H

tests/lean/tst11.lean.expected.out

@@ -6,7 +6,7 @@
 ⊤
   Assumed: a
 a ⊕ a ⊕ a
-@subst : ∀ (A : TypeU) (a b : A) (P : A → Bool), P a → a = b → P b
+@subst : ∀ (A : TypeU') (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/tst17.lean.expected.out

@@ -4,4 +4,4 @@
   Assumed: g
 ∀ a b : Type, ∃ c : Type, g a b = f c
 ∀ a b : Type, ∃ c : Type, g a b = f c : Bool
-∀ (a b : Type), (∀ (x : Type), g a b == f x → ⊥) → ⊥
+∀ (a b : Type), (∀ (x : Type), g a b = f x → ⊥) → ⊥

tests/lean/tst4.lean.expected.out

@@ -10,9 +10,7 @@
   Assumed: EqNice
 @EqNice N n1 n2
 @f N n1 n2 : N
-@congr :
+@congr : ∀ (A B : TypeU') (f g : A → B) (a b : A), @eq (A → B) f g → @eq A a b → @eq B (f a) (g b)
-    ∀ (A : TypeU) (B : A → TypeU) (f g : ∀ x : A, B x) (a b : A),
-      @eq (∀ x : A, B x) f g → @eq A a b → f a == g b
 @f N n1 n2
   Assumed: a
   Assumed: b
@@ -23,7 +21,7 @@
 axiom H1 : @eq N a b ∧ @eq N b c
 theorem Pr : @eq N (g a) (g c) :=
     @congr N
-           (λ x : N, N)
+           N
            g
            g
            a

tests/lean/tst6.lean.expected.out

@@ -6,7 +6,7 @@
   Set: lean::pp::implicit
 variable h : N → N → N
 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) :=
-    @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
+    @congr N N (h a1) (h b1) a2 b2 (@congr N (N → N) h h a1 b1 (@refl (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
@@ -15,7 +15,7 @@ theorem congrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1
 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) :=
     @or_elim (@eq N a b ∧ @eq N b c)
              (@eq N a d ∧ @eq N d c)
-             (h a b == h c b)
+             (@eq N (h a b) (h c b))
              H
              (λ H1 : @eq N a b ∧ @eq N b c,
                 @congrH a

tests/lean/type_inf_bug1.lean

@@ -1,34 +0,0 @@
-import cast
-set_option pp::colors false
-
-check fun (A A': TypeM)
-          (a   : A)
-          (b   : A')
-          (L2  : A' == A),
-   let b' : A        := cast     L2 b,
-       L3 : b == b'  := cast_eq L2 b
-   in L3
-
-check fun (A A': TypeM)
-          (B   : A -> TypeM)
-          (B'  : A' -> TypeM)
-          (f   : forall x : A, B x)
-          (g   : forall x : A', B' x)
-          (a   : A)
-          (b   : A')
-          (H1  : (forall x : A, B x) == (forall x : A', B' x))
-          (H2  : f == g)
-          (H3  : a == b),
-    let L1 : A  == A'                             := type_eq H3,
-        L2 : A' == A                              := symm L1,
-        b' : A                                    := cast L2 b,
-        L3 : b  == b'                             := cast_eq L2 b,
-        L4 : a == b'                              := htrans H3 L3,
-        L5 : f a == f b'                          := congr2 f L4,
-        S1 : (forall x : A', B' x) == (forall x : A, B x) := symm H1,
-        g' : (forall x : A, B x)                      := cast S1 g,
-        L6 : g == g'                              := cast_eq S1 g,
-        L7 : f == g'                              := htrans H2 L6,
-        L8 : f b' == g' b'                        := congr1 b' L7,
-        L9 : f a == g' b'                         := htrans L5 L8
-    in L9

tests/lean/type_inf_bug1.lean.expected.out

@@ -1,40 +0,0 @@
-  Set: pp::colors
-  Set: pp::unicode
-  Imported 'cast'
-  Set: pp::colors
-λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast_eq L2 b in L3 :
-    ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
-λ (A A' : TypeM)
-  (B : A → TypeM)
-  (B' : A' → TypeM)
-  (f : ∀ x : A, B x)
-  (g : ∀ x : A', B' x)
-  (a : A)
-  (b : A')
-  (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
-  (H2 : f == g)
-  (H3 : a == b),
-  let L1 : A == A' := type_eq H3,
-      L2 : A' == A := symm L1,
-      b' : A := cast L2 b,
-      L3 : b == b' := cast_eq L2 b,
-      L4 : a == b' := htrans H3 L3,
-      L5 : f a == f b' := congr2 f L4,
-      S1 : (∀ x : A', B' x) == (∀ x : A, B x) := symm H1,
-      g' : ∀ x : A, B x := cast S1 g,
-      L6 : g == g' := cast_eq S1 g,
-      L7 : f == g' := htrans H2 L6,
-      L8 : f b' == g' b' := congr1 b' L7,
-      L9 : f a == g' b' := htrans L5 L8
-  in L9 :
-    ∀ (A A' : TypeM)
-      (B : A → TypeM)
-      (B' : A' → TypeM)
-      (f : ∀ x : A, B x)
-      (g : ∀ x : A', B' x)
-      (a : A)
-      (b : A')
-      (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
-      (H2 : f == g)
-      (H3 : a == b),
-      f a == cast (symm H1) g (cast (symm (type_eq H3)) b)

tests/lua/env4.lua

@@ -25,8 +25,9 @@ local ok, msg = pcall(function() child:add_definition("val3", Const("Int"), Cons
 assert(not ok)
 print(msg)
 assert(child:normalize(Const("val2")) == Const("val2"))
-child:add_theorem("Th1", HEq(iVal(0), iVal(0)), Const("trivial"))
+local Int = Const("Int")
-child:add_axiom("H1", HEq(Const("x"), iVal(0)))
+child:add_theorem("Th1", mk_eq(Int, iVal(0), iVal(0)), Const("trivial"))
+child:add_axiom("H1", mk_eq(Int, Const("x"), iVal(0)))
 assert(child:has_object("H1"))
 local ctx = context(context(), "x", Const("Int"), iVal(10))
 assert(child:normalize(Var(0), ctx) == iVal(10))

tests/lua/expr5.lua

@@ -3,7 +3,6 @@ n = e:get_body()
 check_error(function() mk_heq(n, Const("a")) end)
 print(Const("a") < Const("b"))
 check_error(function() mk_app(Const("a")) end)
-print(mk_heq(Const("a"), Const("b")))
 print(mk_pi("x", Const("N"), Var(0)))
 print(Pi("x", Const("N"), Const("x")))
 assert(mk_pi("x", Const("N"), Var(0)) == Pi("x", Const("N"), Const("x")))

tests/lua/expr6.lua

@@ -22,10 +22,6 @@ function print_leaves(e, ctx)
       print("abstraction var name: " .. tostring(name))
       print_leaves(domain, ctx)
       print_leaves(body, ctx:extend(name, domain))
-   elseif k == expr_kind.HEq then
-      local lhs, rhs = e:fields()
-      print_leaves(lhs, ctx)
-      print_leaves(rhs, ctx)
    elseif k == expr_kind.Let then
       local name, ty, val, body = e:fields()
       print("let var name: " .. tostring(name))
@@ -43,6 +39,6 @@ local x, y, z = Consts("x, y, z")
 assert(is_expr(f))
 
 local F = fun(h, mk_arrow(N, N),
-              Let(x, h(a), HEq(f(x), h(x))))
+              Let(x, h(a), mk_eq(N, f(x), h(x))))
 print(F)
 print_leaves(F, context())

tests/lua/expr8.lua

@@ -25,7 +25,6 @@ assert(mk_metavar("M"):is_metavar())
 assert(mk_real_value(mpq(10)):is_value())
 assert(not F:has_metavar())
 assert(f(mk_metavar("M")):has_metavar())
-assert(HEq(a, b):is_heq())
 assert(F:num_args() == 3)
 assert(F:arg(0) == f)
 assert(F:arg(1) == g(x, a))

tests/lua/is_prop1.lua

@@ -21,7 +21,7 @@ assert(env:is_proposition(parse_lean([[true -> false]])))
 assert(env:is_proposition(parse_lean([[Nat -> false]])))
 assert(not env:is_proposition(parse_lean([[true -> Nat]])))
 assert(not env:is_proposition(parse_lean([[Type]])))
-assert(env:is_proposition(parse_lean([[0 == 1]])))
+assert(env:is_proposition(parse_lean([[0 = 1]])))
 assert(env:is_proposition(parse_lean([[q]])))
 
 

tests/lua/unify1.lua

@@ -16,7 +16,6 @@ function must_unify(t1, t2)
    assert(s:apply(t1) == s:apply(t2))
 end
 Bool = Const("Bool")
-must_unify(HEq(a, m1), HEq(m2, m2))
 must_unify(Type(), m1)
 must_unify(fun(x, Bool, x), fun(x, Bool, m1))
 must_unify(Pi(x, Bool, x), Pi(x, Bool, m1))