Function assume

src/compute-engine/assume.ts:88–107

(proposition: Expression)

  symbol: string,
  cause?: Expression
): void {
  const def = ce.lookupDefinition(symbol);
  if (isValueDef(def)) recordAssumedType(ce, def.value, cause);
}

/**
 * Infer a promoted type from a value expression.
 * This promotes specific types to more general ones suitable for symbols:
 * - finite_integer -> integer
 * - rational -> real
 * - finite_real_number -> real
 * - complex/imaginary -> number
 */
function inferTypeFromValue(ce: ComputeEngine, value: Expression): BoxedType {
  // finite_integer, integer, etc. -> integer
  if (value.type.matches('integer')) return ce.type('integer');

  // rational -> real
  if (value.type.matches('rational')) return ce.type('real');

  // finite_real_number, real -> real
  if (value.type.matches('real')) return ce.type('real');