lean icon indicating copy to clipboard operation
lean copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

API to set decl_pos

Open bryangingechen opened this issue 5 years ago • 1 comments

It could either be an extra argument to the environment.add_decl function, or a free function set_decl_pos, depending on the constraints in the C++.

From https://github.com/leanprover-community/mathlib/issues/4778

bryangingechen avatar Oct 25 '20 21:10 bryangingechen

A more magic solution might be to set module::scope_pos_info in more places.

gebner avatar Oct 26 '20 09:10 gebner