We have inherited the terminology "constant" from the Lean 4 source code but I think it's not a good term. For example, a function that takes arguments doesn't look like a constant to me.
This issue is about changing the occurrences of "constant" to "declaration" in the code base. "Const" should be changed to "Decl" etc.
We have inherited the terminology "constant" from the Lean 4 source code but I think it's not a good term. For example, a function that takes arguments doesn't look like a constant to me.
This issue is about changing the occurrences of "constant" to "declaration" in the code base. "Const" should be changed to "Decl" etc.