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

chore(library/compiler/csimp): add comment

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-25 18:47:40 -07:00
parent 6b6b6eb96f
commit 8613255ff2
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/compiler/csimp.cpp
View file

@ -328,7 +328,9 @@ class csimp_fn {
return some_expr(mk_app(fn, args));
}
} else {
/* Create jp value */
/* Create jp value for `e`
This kind of join-point is not very useful. It will only help if we decide
to inline the join-point later in some of the branches. */
local_decl fvar_decl = m_lctx.get_local_decl(fvar);
expr jp_val = e;
{