lean-llvm
lean-llvm copied to clipboard
Test that change to `src/llvm_exports.cpp` is sound
This is the change I'm not positive is correct =\
Here is a commit removing various usages of cnstr_get_scalar
and cnstr_set_scalar
right before the commit that removed those two template functions from lean4: https://github.com/leanprover/lean4/commit/16d88b04ea2a8ad445b16636eece7c5e3e08a71d
Those don't end up using cnstr_set
... however, there is other code in the test directories that seems very similar to what we're doing here, e.g. https://github.com/leanprover/lean4/blob/ec9f4b579dc6b4a20407d2735f8ad91de29bfdb5/src/tests/util/object.cpp#L266
So yah, I'm not sure.
Originally posted by @pnwamk in https://github.com/GaloisInc/lean-llvm/pull/16