fact: Definition evalExprTypePrim T := match T with | Integer => PrimInt63.int | BinFloat => PrimFloat.float end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)