3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-03 07:46:23 +00:00

Fix TypeScript compilation errors in RCFNum tests

- Fix type declaration: use ReturnType to get RCFNum type from Context
- Add explicit type annotation to forEach parameter
- Add RCFNum to imports

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-17 20:02:55 +00:00
parent b5b1af3de7
commit 08a8b1cc71

View file

@ -1,7 +1,7 @@
import assert from 'assert';
import asyncToArray from 'iter-tools/methods/async-to-array';
import { init, killThreads } from '../jest';
import { Arith, Bool, Model, Quantifier, Z3AssertionError, Z3HighLevel, AstVector } from './types';
import { Arith, Bool, Model, Quantifier, Z3AssertionError, Z3HighLevel, AstVector, RCFNum } from './types';
import { expectType } from 'ts-expect';
// this should not be necessary but there may be a Jest bug
@ -1986,7 +1986,7 @@ describe('high-level', () => {
});
describe('RCFNum', () => {
let RCFNum: Z3HighLevel['RCFNum'];
let RCFNum: ReturnType<typeof api.Context<'rcf'>>['RCFNum'];
beforeEach(() => {
({ RCFNum } = api.Context('rcf'));
@ -2145,7 +2145,7 @@ describe('high-level', () => {
expect(roots.length).toBe(2);
// All roots should be algebraic
roots.forEach(root => {
roots.forEach((root: RCFNum<'rcf'>) => {
expect(root.isAlgebraic()).toBe(true);
});