Skip to content

Commit

Permalink
chore: Remove unused variables from kernel
Browse files Browse the repository at this point in the history
when I build lean locally, I get a nice and warning-free build
experience with the exception of these two unused variables. They can
probably go?
  • Loading branch information
nomeata authored and leodemoura committed Sep 27, 2023
1 parent 75f91f3 commit 06e0577
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 4 deletions.
2 changes: 0 additions & 2 deletions src/kernel/inductive.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -614,7 +614,6 @@ class add_inductive_fn {
d_idx++;
}
/* First, populate the field m_minors */
unsigned minor_idx = 1;
d_idx = 0;
for (inductive_type const & ind_type : m_ind_types) {
name ind_type_name = ind_type.get_name();
Expand Down Expand Up @@ -666,7 +665,6 @@ class add_inductive_fn {
name minor_name = cnstr_name.replace_prefix(ind_type_name, name());
expr minor = mk_local_decl(minor_name, minor_ty);
m_rec_infos[d_idx].m_minors.push_back(minor);
minor_idx++;
}
d_idx++;
}
Expand Down
2 changes: 0 additions & 2 deletions src/library/compiler/csimp.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -302,12 +302,10 @@ class csimp_fn {
}

expr get_minor_body(expr e, buffer<expr> & xs) {
unsigned i = 0;
while (is_lambda(e)) {
expr d = instantiate_rev(binding_domain(e), xs.size(), xs.data());
expr x = m_lctx.mk_local_decl(ngen(), binding_name(e), d, binding_info(e));
xs.push_back(x);
i++;
e = binding_body(e);
}
return instantiate_rev(e, xs.size(), xs.data());
Expand Down

0 comments on commit 06e0577

Please sign in to comment.