From 7cb90bedfe61a56e04d12656465369cd8651f026 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 12 Jul 2018 10:55:28 +0200 Subject: [PATCH] fix(src/kernel/old_type_checker): literals in inductive defs --- src/kernel/old_type_checker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/old_type_checker.cpp b/src/kernel/old_type_checker.cpp index 6db4d15235..58648f5447 100644 --- a/src/kernel/old_type_checker.cpp +++ b/src/kernel/old_type_checker.cpp @@ -254,7 +254,7 @@ expr old_type_checker::infer_type_core(expr const & e, bool infer_only) { case expr_kind::Pi: r = infer_pi(e, infer_only); break; case expr_kind::App: r = infer_app(e, infer_only); break; case expr_kind::Let: r = infer_let(e, infer_only); break; - case expr_kind::Lit: r = infer_let(e, infer_only); break; + case expr_kind::Lit: r = lit_type(e); break; case expr_kind::Quote: throw_found_quote(m_env); }