From 2008ddc7d02bf0b72bf9715d6141551e35ef70d9 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 3 Jul 2020 09:32:11 +0000 Subject: [PATCH] =?UTF-8?q?fix(library/type=5Fcontext):=20do=20not=20unify?= =?UTF-8?q?=20`(1=20:=20=E2=84=95)`=20with=20`(1=20:=20=E2=84=A4)`=20(#376?= =?UTF-8?q?)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #362. --- src/library/type_context.cpp | 5 +++-- tests/lean/run/362c.lean | 2 ++ tests/lean/widget/widget4.input.expected.out | 2 +- 3 files changed, 6 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/362c.lean diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 1c5e7849e6..dbaa25bf38 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -3102,8 +3102,6 @@ lbool type_context_old::try_numeral_eq_numeral(expr const & t, expr const & s) { if (!n1) return l_undef; optional n2 = eval_num(s); if (!n2) return l_undef; - if (!is_nat_type(whnf(infer(t)))) - return l_undef; if (*n1 != *n2) return l_false; else if (to_small_num(t) && to_small_num(s)) @@ -3117,6 +3115,9 @@ lbool type_context_old::try_nat_offset_cnstrs(expr const & t, expr const & s) { /* We should not use this feature when transparency_mode is none. See issue #1295 */ if (m_transparency_mode == transparency_mode::None) return l_undef; + // Only special-case natural numbers, see https://github.com/leanprover-community/lean/issues/362 + if (!is_nat_type(whnf(infer(t))) || !is_nat_type(whnf(infer(s)))) + return l_undef; lbool r; r = try_offset_eq_offset(t, s); if (r != l_undef) return r; diff --git a/tests/lean/run/362c.lean b/tests/lean/run/362c.lean new file mode 100644 index 0000000000..153437ddde --- /dev/null +++ b/tests/lean/run/362c.lean @@ -0,0 +1,2 @@ +open tactic +#eval success_if_fail $ unify `(1 : ℕ) `(1 : ℤ) \ No newline at end of file diff --git a/tests/lean/widget/widget4.input.expected.out b/tests/lean/widget/widget4.input.expected.out index 1b02c0363f..b9ba6b4c22 100644 --- a/tests/lean/widget/widget4.input.expected.out +++ b/tests/lean/widget/widget4.input.expected.out @@ -1,3 +1,3 @@ {"msgs":[{"caption":"","file_name":"widget4.lean","pos_col":0,"pos_line":3,"severity":"information","text":"(widget)","widget":{"column":0,"id":3,"line":3}}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} -{"response":"ok","seq_num":1,"widget":{"column":0,"html":{"c":[{"a":{"className":"list pl0"},"c":[{"a":{"className":"lh-copy"},"c":[{"a":{"className":"goal-goals"},"c":["expected type:"],"t":"strong"}],"t":"li"},{"a":{"className":"lh-copy"},"c":[{"c":[{"a":{"className":"list pl0 font-code","key":"419198192"},"c":[{"a":{"key":"_mlocal._fresh.10.70"},"c":[{"a":{"className":"goal-vdash b"},"c":["⊢ "],"t":"span"},{"c":[{"c":[{"a":{"className":"expr","key":"695702567"},"c":[{"a":{"className":"expr-boundary","key":"[]"},"c":[{"a":{"key":"true"},"c":["true"],"e":{"onClick":{"h":2,"r":[6,5,4,3]},"onMouseEnter":{"h":1,"r":[6,5,4,3]}},"t":"span"}],"t":"span"}],"e":{"onMouseLeave":{"h":0,"r":[6,5,4,3]}},"t":"span"}]}]}],"t":"li"}],"t":"ul"}]}],"t":"li"}],"t":"ul"}]},"id":3,"line":3}} +{"response":"ok","seq_num":1,"widget":{"column":0,"html":{"c":[{"a":{"className":"list pl0"},"c":[{"a":{"className":"lh-copy"},"c":[{"a":{"className":"goal-goals"},"c":["expected type:"],"t":"strong"}],"t":"li"},{"a":{"className":"lh-copy"},"c":[{"c":[{"a":{"className":"list pl0 font-code","key":"417262892"},"c":[{"a":{"key":"_mlocal._fresh.10.100"},"c":[{"a":{"className":"goal-vdash b"},"c":["⊢ "],"t":"span"},{"c":[{"c":[{"a":{"className":"expr","key":"695702567"},"c":[{"a":{"className":"expr-boundary","key":"[]"},"c":[{"a":{"key":"true"},"c":["true"],"e":{"onClick":{"h":2,"r":[6,5,4,3]},"onMouseEnter":{"h":1,"r":[6,5,4,3]}},"t":"span"}],"t":"span"}],"e":{"onMouseLeave":{"h":0,"r":[6,5,4,3]}},"t":"span"}]}]}],"t":"li"}],"t":"ul"}]}],"t":"li"}],"t":"ul"}]},"id":3,"line":3}}