Yiyun Liu
Yiyun Liu
Consider the following program: ```C #include #include #include #pragma CHECKED_SCOPE ON int main(int argc, nt_array_ptr argv checked[] : count(argc)) { nt_array_ptr str = "hello"; // forget the precise bound information...
Coq version: 8.15.0 Hammer version: 1.3.2+8.15 Here is a minimal example. test.v: ```coq Theorem wrong : 1 = 2. (* placeholder *) idtac. Qed. ``` test2.v: ```coq Require Import test....
Hi, The code [here](https://gist.github.com/yiyunliu/587fb2c77e9e58f9b41ae285476a365f) joins two 6-dimension boxes. For each dimension, the width is no more than 100. Despite the coefficients, constants, dimensions being relatively small, ELINA throws overflow exception...
#### Description of the problem Here's the example program: ```coq From Ltac2 Require Import Ltac2. Ltac2 Eval () 1. ``` Here's the error message: ``` File "./test4.v", line 2, characters...
The following program reads a long int, assigns the long int to an unsigned long, then branches on whether the unsigned long is equal to the constant `10086`: ```C #include...
I did include a negative test file which returns exit code 1 for the fixed elimEta and 2 for the buggy one. However, I need to test Wen's example before...
Once typeclass support is properly implemented, we should no longer drop dictionaries (term level) and class constraints (type level), with the exception of Eq, Ord, Numerical (Num, Integral, etc.). While...
A summary of what I did: - The redefined `gather_atoms` isn't used for some reason even though ett_ind is required and imported. I included an extra import at the bottom...
This PR adds `#[export]` to the coq files in the headers directory. I also made minor tweaks such as `Omega -> lia` so the code compiles with coq 8.17.