fact: Definition SIOpToFunction OP := match OP with | ADD => Int32.add | SUB => Int32.sub | MUL => Int32.mul | DIV => Int32.quot end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)