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

fix(library/equations_compiler/util): typo

Browse source
This commit is contained in:
Leonardo de Moura 2017-11-22 12:50:23 -08:00
parent 7c35a25169
commit 01bbf27fb0
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/equations_compiler/util.cpp
View file

@ -353,7 +353,7 @@ static environment add_equation_lemma(environment const & env, options const & o
std::tie(new_env, new_type) = abstract_rhs_nested_proofs(new_env, mctx, lctx, f_actual_name, new_type);
}
try {
std::tie(new_env, r) = mk_aux_definition(new_env, mctx, lctx, new_eqn_name, new_type, new_value);
std::tie(new_env, r) = mk_aux_lemma(new_env, mctx, lctx, new_eqn_name, new_type, new_value);
if (is_rfl_lemma(new_type, new_value))
new_env = mark_rfl_lemma(new_env, new_eqn_name);
new_env = add_eqn_lemma(new_env, new_eqn_name);