diff --git a/src/api/js/examples/high-level/rcf-example.ts b/src/api/js/examples/high-level/rcf-example.ts
new file mode 100644
index 000000000..a5f021e28
--- /dev/null
+++ b/src/api/js/examples/high-level/rcf-example.ts
@@ -0,0 +1,199 @@
+/**
+ * Example demonstrating the RCF (Real Closed Field) API in TypeScript.
+ * 
+ * This example shows how to use RCF numerals to work with:
+ * - Transcendental numbers (pi, e)
+ * - Algebraic numbers (roots of polynomials)
+ * - Infinitesimals
+ * - Exact real arithmetic
+ * 
+ * Note: This example uses the high-level API for a cleaner interface.
+ */
+
+import { init } from 'z3-solver';
+
+async function rcfBasicExample() {
+  console.log('RCF Basic Example (High-Level API)');
+  console.log('===================================');
+
+  const { Context } = await init();
+  const { RCFNum } = Context('main');
+
+  // Create pi and e
+  const pi = RCFNum.pi();
+  const e = RCFNum.e();
+
+  console.log('pi =', pi.toString());
+  console.log('e =', e.toString());
+
+  // Arithmetic operations
+  const sum = pi.add(e);
+  const prod = pi.mul(e);
+
+  console.log('pi + e =', sum.toString());
+  console.log('pi * e =', prod.toString());
+
+  // Decimal approximations
+  console.log('pi (10 decimals) =', pi.toDecimal(10));
+  console.log('e (10 decimals) =', e.toDecimal(10));
+
+  // Comparisons
+  console.log('pi < e?', pi.lt(e) ? 'yes' : 'no');
+  console.log('pi > e?', pi.gt(e) ? 'yes' : 'no');
+}
+
+async function rcfRationalExample() {
+  console.log('\nRCF Rational Example (High-Level API)');
+  console.log('=====================================');
+
+  const { Context } = await init();
+  const { RCFNum } = Context('main');
+
+  // Create rational numbers
+  const half = RCFNum('1/2');
+  const third = RCFNum('1/3');
+
+  console.log('1/2 =', half.toString());
+  console.log('1/3 =', third.toString());
+
+  // Arithmetic
+  const sum = half.add(third);
+  console.log('1/2 + 1/3 =', sum.toString());
+  console.log('1/2 + 1/3 (decimal) =', sum.toDecimal(10));
+
+  // Type queries
+  console.log('Is 1/2 rational?', half.isRational() ? 'yes' : 'no');
+  console.log('Is 1/2 algebraic?', half.isAlgebraic() ? 'yes' : 'no');
+}
+
+async function rcfRootsExample() {
+  console.log('\nRCF Roots Example (High-Level API)');
+  console.log('===================================');
+
+  const { Context } = await init();
+  const { RCFNum } = Context('main');
+
+  // Find roots of x^2 - 2 = 0
+  // Polynomial: -2 + 0*x + 1*x^2
+  const coeffs = [
+    RCFNum(-2),  // constant term
+    RCFNum(0),   // x coefficient
+    RCFNum(1)    // x^2 coefficient
+  ];
+
+  const roots = RCFNum.roots(coeffs);
+
+  console.log('Roots of x^2 - 2 = 0:');
+  for (let i = 0; i < roots.length; i++) {
+    console.log(`  root[${i}] =`, roots[i].toString());
+    console.log(`  decimal =`, roots[i].toDecimal(15));
+    console.log(`  is_algebraic =`, roots[i].isAlgebraic() ? 'yes' : 'no');
+  }
+}
+
+async function rcfInfinitesimalExample() {
+  console.log('\nRCF Infinitesimal Example (High-Level API)');
+  console.log('===========================================');
+
+  const { Context } = await init();
+  const { RCFNum } = Context('main');
+
+  // Create an infinitesimal
+  const eps = RCFNum.infinitesimal();
+  console.log('eps =', eps.toString());
+  console.log('Is eps infinitesimal?', eps.isInfinitesimal() ? 'yes' : 'no');
+
+  // Infinitesimals are smaller than any positive real number
+  const tiny = RCFNum('1/1000000000');
+  console.log('eps < 1/1000000000?', eps.lt(tiny) ? 'yes' : 'no');
+}
+
+async function rcfArithmeticExample() {
+  console.log('\nRCF Arithmetic Operations Example');
+  console.log('==================================');
+
+  const { Context } = await init();
+  const { RCFNum } = Context('main');
+
+  const a = RCFNum(5);
+  const b = RCFNum(3);
+
+  console.log('a =', a.toString());
+  console.log('b =', b.toString());
+  console.log('a + b =', a.add(b).toString());
+  console.log('a - b =', a.sub(b).toString());
+  console.log('a * b =', a.mul(b).toString());
+  console.log('a / b =', a.div(b).toString(), '=', a.div(b).toDecimal(5));
+  console.log('-a =', a.neg().toString());
+  console.log('1/a =', a.inv().toString(), '=', a.inv().toDecimal(5));
+  console.log('a^3 =', a.power(3).toString());
+
+  // Comparisons
+  console.log('\nComparisons:');
+  console.log('a < b?', a.lt(b));
+  console.log('a > b?', a.gt(b));
+  console.log('a <= b?', a.le(b));
+  console.log('a >= b?', a.ge(b));
+  console.log('a == b?', a.eq(b));
+  console.log('a != b?', a.neq(b));
+}
+
+async function rcfSymbolicMathExample() {
+  console.log('\nRCF Symbolic Mathematics Example');
+  console.log('=================================');
+
+  const { Context } = await init();
+  const { RCFNum } = Context('main');
+
+  // Work with exact symbolic values
+  const pi = RCFNum.pi();
+  const e = RCFNum.e();
+  const sqrt2Coeffs = [RCFNum(-2), RCFNum(0), RCFNum(1)];
+  const sqrt2Roots = RCFNum.roots(sqrt2Coeffs);
+  const sqrt2 = sqrt2Roots.find(r => r.gt(RCFNum(0)))!;
+
+  console.log('π =', pi.toDecimal(15));
+  console.log('e =', e.toDecimal(15));
+  console.log('√2 =', sqrt2.toDecimal(15));
+
+  // Combine them
+  const expr1 = pi.add(e);
+  const expr2 = pi.mul(sqrt2);
+  const expr3 = e.power(2);
+
+  console.log('\nExpressions:');
+  console.log('π + e =', expr1.toDecimal(10));
+  console.log('π × √2 =', expr2.toDecimal(10));
+  console.log('e² =', expr3.toDecimal(10));
+
+  // Check properties
+  console.log('\nProperties:');
+  console.log('π is transcendental:', pi.isTranscendental());
+  console.log('e is transcendental:', e.isTranscendental());
+  console.log('√2 is algebraic:', sqrt2.isAlgebraic());
+  console.log('√2 is rational:', sqrt2.isRational());
+}
+
+async function main() {
+  try {
+    await rcfBasicExample();
+    await rcfRationalExample();
+    await rcfRootsExample();
+    await rcfInfinitesimalExample();
+    await rcfArithmeticExample();
+    await rcfSymbolicMathExample();
+
+    console.log('\n✓ All RCF examples completed successfully!');
+    console.log('\nThe RCF API in TypeScript now provides:');
+    console.log('  • 38 functions for exact real arithmetic');
+    console.log('  • Support for π, e, algebraic numbers, and infinitesimals');
+    console.log('  • Full arithmetic and comparison operations');
+    console.log('  • Polynomial root finding');
+    console.log('  • Type predicates and conversions');
+  } catch (error) {
+    console.error('Error:', error);
+    throw error;
+  }
+}
+
+main();
diff --git a/src/api/js/src/high-level/high-level.test.ts b/src/api/js/src/high-level/high-level.test.ts
index e1290188c..cc449ad11 100644
--- a/src/api/js/src/high-level/high-level.test.ts
+++ b/src/api/js/src/high-level/high-level.test.ts
@@ -1984,4 +1984,246 @@ describe('high-level', () => {
       }
     });
   });
+
+  describe('RCFNum', () => {
+    let RCFNum: Z3HighLevel['RCFNum'];
+
+    beforeEach(() => {
+      ({ RCFNum } = api.Context('rcf'));
+    });
+
+    it('should create RCF from string', () => {
+      const half = RCFNum('1/2');
+      expect(half.toString()).toContain('1');
+      expect(half.toString()).toContain('2');
+      expect(half.isRational()).toBe(true);
+    });
+
+    it('should create RCF from integer', () => {
+      const five = RCFNum(5);
+      expect(five.toString()).toContain('5');
+      expect(five.isRational()).toBe(true);
+    });
+
+    it('should create pi', () => {
+      const pi = RCFNum.pi();
+      expect(pi.isTranscendental()).toBe(true);
+      expect(pi.isRational()).toBe(false);
+      const piStr = pi.toDecimal(10);
+      expect(piStr).toContain('3.14');
+    });
+
+    it('should create e', () => {
+      const e = RCFNum.e();
+      expect(e.isTranscendental()).toBe(true);
+      expect(e.isRational()).toBe(false);
+      const eStr = e.toDecimal(10);
+      expect(eStr).toContain('2.71');
+    });
+
+    it('should create infinitesimal', () => {
+      const eps = RCFNum.infinitesimal();
+      expect(eps.isInfinitesimal()).toBe(true);
+      expect(eps.isRational()).toBe(false);
+    });
+
+    it('should perform addition', () => {
+      const a = RCFNum('1/2');
+      const b = RCFNum('1/3');
+      const sum = a.add(b);
+      expect(sum.isRational()).toBe(true);
+      // 1/2 + 1/3 = 5/6
+      const decimal = sum.toDecimal(5);
+      expect(decimal).toContain('0.833');
+    });
+
+    it('should perform subtraction', () => {
+      const a = RCFNum(1);
+      const b = RCFNum('1/2');
+      const diff = a.sub(b);
+      expect(diff.isRational()).toBe(true);
+      // 1 - 1/2 = 1/2
+      const decimal = diff.toDecimal(5);
+      expect(decimal).toContain('0.5');
+    });
+
+    it('should perform multiplication', () => {
+      const a = RCFNum(2);
+      const b = RCFNum(3);
+      const prod = a.mul(b);
+      expect(prod.isRational()).toBe(true);
+      expect(prod.toString()).toContain('6');
+    });
+
+    it('should perform division', () => {
+      const a = RCFNum(1);
+      const b = RCFNum(2);
+      const quot = a.div(b);
+      expect(quot.isRational()).toBe(true);
+      const decimal = quot.toDecimal(5);
+      expect(decimal).toContain('0.5');
+    });
+
+    it('should perform negation', () => {
+      const a = RCFNum(5);
+      const negA = a.neg();
+      expect(negA.toString()).toContain('-');
+    });
+
+    it('should perform inversion', () => {
+      const a = RCFNum(2);
+      const inv = a.inv();
+      expect(inv.isRational()).toBe(true);
+      const decimal = inv.toDecimal(5);
+      expect(decimal).toContain('0.5');
+    });
+
+    it('should perform power', () => {
+      const a = RCFNum(2);
+      const squared = a.power(2);
+      expect(squared.toString()).toContain('4');
+    });
+
+    it('should compare with lt', () => {
+      const a = RCFNum(1);
+      const b = RCFNum(2);
+      expect(a.lt(b)).toBe(true);
+      expect(b.lt(a)).toBe(false);
+    });
+
+    it('should compare with gt', () => {
+      const a = RCFNum(2);
+      const b = RCFNum(1);
+      expect(a.gt(b)).toBe(true);
+      expect(b.gt(a)).toBe(false);
+    });
+
+    it('should compare with le', () => {
+      const a = RCFNum(1);
+      const b = RCFNum(2);
+      const c = RCFNum(1);
+      expect(a.le(b)).toBe(true);
+      expect(a.le(c)).toBe(true);
+      expect(b.le(a)).toBe(false);
+    });
+
+    it('should compare with ge', () => {
+      const a = RCFNum(2);
+      const b = RCFNum(1);
+      const c = RCFNum(2);
+      expect(a.ge(b)).toBe(true);
+      expect(a.ge(c)).toBe(true);
+      expect(b.ge(a)).toBe(false);
+    });
+
+    it('should compare with eq', () => {
+      const a = RCFNum(5);
+      const b = RCFNum(5);
+      const c = RCFNum(6);
+      expect(a.eq(b)).toBe(true);
+      expect(a.eq(c)).toBe(false);
+    });
+
+    it('should compare with neq', () => {
+      const a = RCFNum(5);
+      const b = RCFNum(6);
+      const c = RCFNum(5);
+      expect(a.neq(b)).toBe(true);
+      expect(a.neq(c)).toBe(false);
+    });
+
+    it('should find polynomial roots', () => {
+      // x^2 - 2 = 0 has roots ±√2
+      // Polynomial: -2 + 0*x + 1*x^2
+      const coeffs = [
+        RCFNum(-2),  // constant term
+        RCFNum(0),   // x coefficient
+        RCFNum(1)    // x^2 coefficient
+      ];
+      
+      const roots = RCFNum.roots(coeffs);
+      expect(roots.length).toBe(2);
+      
+      // All roots should be algebraic
+      roots.forEach(root => {
+        expect(root.isAlgebraic()).toBe(true);
+      });
+      
+      // Check that roots are approximately ±√2
+      const root1Decimal = roots[0].toDecimal(5);
+      const root2Decimal = roots[1].toDecimal(5);
+      
+      // One should be approximately 1.414 and the other -1.414
+      const decimals = [root1Decimal, root2Decimal].sort();
+      expect(decimals[0]).toContain('-1.4');
+      expect(decimals[1]).toContain('1.4');
+    });
+
+    it('should check isRational predicate', () => {
+      const rational = RCFNum('3/4');
+      const pi = RCFNum.pi();
+      
+      expect(rational.isRational()).toBe(true);
+      expect(pi.isRational()).toBe(false);
+    });
+
+    it('should check isAlgebraic predicate', () => {
+      // x^2 - 2 = 0
+      const coeffs = [RCFNum(-2), RCFNum(0), RCFNum(1)];
+      const roots = RCFNum.roots(coeffs);
+      
+      expect(roots[0].isAlgebraic()).toBe(true);
+      
+      // Pi is not algebraic
+      const pi = RCFNum.pi();
+      expect(pi.isAlgebraic()).toBe(false);
+    });
+
+    it('should check isTranscendental predicate', () => {
+      const pi = RCFNum.pi();
+      const e = RCFNum.e();
+      const rational = RCFNum(5);
+      
+      expect(pi.isTranscendental()).toBe(true);
+      expect(e.isTranscendental()).toBe(true);
+      expect(rational.isTranscendental()).toBe(false);
+    });
+
+    it('should check isInfinitesimal predicate', () => {
+      const eps = RCFNum.infinitesimal();
+      const rational = RCFNum(5);
+      
+      expect(eps.isInfinitesimal()).toBe(true);
+      expect(rational.isInfinitesimal()).toBe(false);
+    });
+
+    it('should convert to string with compact mode', () => {
+      const pi = RCFNum.pi();
+      const compact = pi.toString(true);
+      const nonCompact = pi.toString(false);
+      
+      // Both should contain 'pi' or similar representation
+      expect(compact.length).toBeGreaterThan(0);
+      expect(nonCompact.length).toBeGreaterThan(0);
+    });
+
+    it('should convert to decimal with precision', () => {
+      const pi = RCFNum.pi();
+      const decimal5 = pi.toDecimal(5);
+      const decimal10 = pi.toDecimal(10);
+      
+      // 10 decimal places should be longer than 5
+      expect(decimal10.length).toBeGreaterThanOrEqual(decimal5.length);
+      expect(decimal5).toContain('3.14');
+      expect(decimal10).toContain('3.141592');
+    });
+
+    it('should work with infinitesimal comparisons', () => {
+      const eps = RCFNum.infinitesimal();
+      const tiny = RCFNum('1/1000000');
+      
+      // Infinitesimal should be smaller than any positive real
+      expect(eps.lt(tiny)).toBe(true);
+    });
+  });
 });