equal
deleted
inserted
replaced
28 hypreal :: {ord, zero, one, plus, times, minus, inverse} |
28 hypreal :: {ord, zero, one, plus, times, minus, inverse} |
29 |
29 |
30 defs |
30 defs |
31 |
31 |
32 hypreal_zero_def |
32 hypreal_zero_def |
33 "0 == Abs_hypreal(hyprel``{%n::nat. (Numeral0::real)})" |
33 "0 == Abs_hypreal(hyprel``{%n::nat. (0::real)})" |
34 |
34 |
35 hypreal_one_def |
35 hypreal_one_def |
36 "1 == Abs_hypreal(hyprel``{%n::nat. (Numeral1::real)})" |
36 "1 == Abs_hypreal(hyprel``{%n::nat. (1::real)})" |
37 |
37 |
38 hypreal_minus_def |
38 hypreal_minus_def |
39 "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})" |
39 "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})" |
40 |
40 |
41 hypreal_diff_def |
41 hypreal_diff_def |
42 "x - y == x + -(y::hypreal)" |
42 "x - y == x + -(y::hypreal)" |
43 |
43 |
44 hypreal_inverse_def |
44 hypreal_inverse_def |
45 "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). |
45 "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). |
46 hyprel``{%n. if X n = Numeral0 then Numeral0 else inverse (X n)})" |
46 hyprel``{%n. if X n = 0 then 0 else inverse (X n)})" |
47 |
47 |
48 hypreal_divide_def |
48 hypreal_divide_def |
49 "P / Q::hypreal == P * inverse Q" |
49 "P / Q::hypreal == P * inverse Q" |
50 |
50 |
51 constdefs |
51 constdefs |