michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/simplifier): fix style

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-26 00:36:17 -08:00
parent 844572c382
commit 89bb5fbf19
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/simplifier/simplifier.cpp
View file

@ -337,7 +337,7 @@ class simplifier_fn {
*/
optional<expr> mk_hcongr_th(expr const & f_type, expr const & new_f_type, expr const & f, expr const & new_f,
expr const & Heq_f, expr const & a, result const & new_a) {
// TODO: make the following code more "customizable".
// TODO(Leo): make the following code more "flexible".
// We should be able to "install" new custom congruence theorem
if (is_eq_fn(f) && is_eq_fn(new_f)) {
return mk_typem_congr_th(mk_eq_hcongr_fn(), a, new_a);