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

fix(library/compiler/compiler): typo

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-28 15:34:58 -08:00
parent 1f3201dca1
commit 371baf2002
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/compiler.cpp
View file

@ -91,7 +91,7 @@ static environment cache_stage2(environment env, comp_decls const & ds) {
expr v = d.snd();
expr t = ll_infer_type(env, v);
unsigned arity = get_num_nested_lambdas(v);
v = ensure_arity(t, arity);
t = ensure_arity(t, arity);
lean_trace(name({"compiler", "stage2"}), tout() << n << " : " << t << "\n";);
env = register_stage2_decl(env, n, t, v);
}