search

leanprover-community / lean

Lean 3 Theorem Prover (community fork)
http://leanprover-community.github.io/
Apache License 2.0
435 stars 80 forks source link

API to set decl_pos #486

Open bryangingechen opened 4 years ago

bryangingechen commented 4 years ago

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

gebner commented 4 years ago

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