From 081dff288f40ddbef3780d956e61984078e7eed3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Apr 2022 13:12:53 -0700 Subject: [PATCH] fix: debug build --- src/library/constructions/projection.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index b3ac5414af..9bac6490bc 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -31,7 +31,6 @@ static bool is_prop(expr type) { } environment mk_projections(environment const & env, name const & n, buffer const & proj_names, bool inst_implicit) { - lean_assert(proj_names.size() == infer_kinds.size()); local_ctx lctx; name_generator ngen = mk_constructions_name_generator(); constant_info ind_info = env.get(n);