Go backward to C.5 Rational Numbers Go up to C Logic Evaluator Definitions Go forward to C.7 Complex Numbers

C.6 Real 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 $
// ----------------------------------------------------------------