We are currently working on "coq-of-rust" to improve support for constant definitions by handling them as functions without parameters.

This allows for handling special cases like constants in parametrized "impl" which were out of reach before.

Comments