(* Adding two real numbers just requires pointwise addition of the
approximations. The proof that the resulting sequence is Cauchy is the standard
one: to obtain an approximation up to eps it is necessary to approximate both
(* Adding two real numbers just requires pointwise addition of the
approximations. The proof that the resulting sequence is Cauchy is the standard
one: to obtain an approximation up to eps it is necessary to approximate both
definition Rplus_: R_ → R_ → R_ ≝
λr1,r2. mk_R_ (λn. r1 n + r2 n) ….
#eps
definition Rplus_: R_ → R_ → R_ ≝
λr1,r2. mk_R_ (λn. r1 n + r2 n) ….
#eps
a program that given an initial state returns its trace. To write that function,
we first write a computable version of next, called step. *)
definition step: state → option state ≝
a program that given an initial state returns its trace. To write that function,
we first write a computable version of next, called step. *)
definition step: state → option state ≝