diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index c68e803f9..489d4acdb 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -462,7 +462,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } function from(primitive: boolean): Bool; - function from(primitive: number | CoercibleRational): RatNum; + function from(primitive: number): IntNum | RatNum; + function from(primitive: CoercibleRational): RatNum; function from(primitive: bigint): IntNum; function from>(expr: T): T; function from(expr: CoercibleToExpr): AnyExpr; diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index eae81ff98..d8bda01a1 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -184,9 +184,13 @@ export interface Context { * @category Functions */ from(primitive: boolean): Bool; /** - * Coerce a number or rational into a Real expression + * Coerce a number to an Int or Real expression (integral numbers become Ints) * @category Functions */ - from(primitive: number | CoercibleRational): RatNum; + from(primitive: number): IntNum | RatNum; + /** + * Coerce a rational into a Real expression + * @category Functions */ + from(primitive: CoercibleRational): RatNum; /** * Coerce a big number into a Integer expression * @category Functions */