Go backward to C.5 Rational Numbers Go up to C Logic Evaluator Definitions Go forward to C.7 Complex Numbers |
// ---------------------------------------------------------------- // $Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp $ // the real numbers (faked by rationals) // // (c) 1999, Wolfgang Schreiner, see file COPYRIGHT // http://www.risc.uni-linz.ac.at/software/formal // ---------------------------------------------------------------- read rational; pred R(x) <=> Q(x); fun R(x: N) = @(Z(x), Z1); fun R0 = Q0; fun R1 = Q1; fun R2 = Q2; fun +R(x: R, y: R) = +Q(x, y); fun *R(x: R, y: R) = *Q(x, y); fun -R(x: R) = -Q(x); fun -R(x: R, y: R) = -Q(x, y); fun ^-1R(x: R) = ^-1Q(x); fun /R(x: R, y: R) = /Q(x, y); pred <=R(x: R, y: R) <=> <=Q(x, y); // ---------------------------------------------------------------- // $Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp $ // ----------------------------------------------------------------