3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00

JS api: fix type for from (#6103)

* JS api: fix type for from

* whitespace
This commit is contained in:
Kevin Gibbons 2022-06-22 14:51:40 -07:00 committed by GitHub
parent c15a000d9b
commit 352666b19f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 8 additions and 3 deletions

View file

@ -462,7 +462,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
} }
function from(primitive: boolean): Bool<Name>; function from(primitive: boolean): Bool<Name>;
function from(primitive: number | CoercibleRational): RatNum<Name>; function from(primitive: number): IntNum<Name> | RatNum<Name>;
function from(primitive: CoercibleRational): RatNum<Name>;
function from(primitive: bigint): IntNum<Name>; function from(primitive: bigint): IntNum<Name>;
function from<T extends Expr<Name>>(expr: T): T; function from<T extends Expr<Name>>(expr: T): T;
function from(expr: CoercibleToExpr<Name>): AnyExpr<Name>; function from(expr: CoercibleToExpr<Name>): AnyExpr<Name>;

View file

@ -184,9 +184,13 @@ export interface Context<Name extends string = 'main'> {
* @category Functions */ * @category Functions */
from(primitive: boolean): Bool<Name>; from(primitive: boolean): Bool<Name>;
/** /**
* Coerce a number or rational into a Real expression * Coerce a number to an Int or Real expression (integral numbers become Ints)
* @category Functions */ * @category Functions */
from(primitive: number | CoercibleRational): RatNum<Name>; from(primitive: number): IntNum<Name> | RatNum<Name>;
/**
* Coerce a rational into a Real expression
* @category Functions */
from(primitive: CoercibleRational): RatNum<Name>;
/** /**
* Coerce a big number into a Integer expression * Coerce a big number into a Integer expression
* @category Functions */ * @category Functions */