lean-llvm icon indicating copy to clipboard operation
lean-llvm copied to clipboard

Test that change to `src/llvm_exports.cpp` is sound

Open pnwamk opened this issue 4 years ago • 0 comments

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

pnwamk avatar Apr 30 '20 18:04 pnwamk