(* The only primitive data types of Matita are dependent products and universes.
So far every other user defined data type has been an inductive type. An
(* The only primitive data types of Matita are dependent products and universes.
So far every other user defined data type has been an inductive type. An
(* 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 ≝