leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: Is there code for X?

Topic: decl_pos and decl_olean for current file


Tsuru (Nov 08 2021 at 11:25):

environment.decl_pos and environment.decl_olean can be used for imported files only, and return none for declarations in the current file.
Is there any function that can get the position of declarations in the current file (like decl_pos)? Also, is there any function that can get the path of the current file (like decl_olean)?


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll