max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix warning

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-11 11:14:02 -08:00
parent 38fc8a520d
commit 34178034a0
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/print.cpp
View file

@ -68,7 +68,7 @@ static name cleanup_name(name const & n) {
return n;
}
pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type) {
pair<expr, expr> binding_body_fresh(expr const & b, bool /* preserve_type */) {
lean_assert(is_binding(b));
name n = cleanup_name(binding_name(b));
n = pick_unused_name(binding_body(b), n);
@ -76,7 +76,7 @@ pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type) {
return mk_pair(instantiate(binding_body(b), c), c);
}
pair<expr, expr> let_body_fresh(expr const & b, bool preserve_type) {
pair<expr, expr> let_body_fresh(expr const & b, bool /* preserve_type */) {
lean_assert(is_let(b));
name n = cleanup_name(let_name(b));
n = pick_unused_name(let_body(b), n);