let rec int_to_real_aux n =
match n with
0 -> _R0 (* o forse R0 + R0 ????? *)
+ | 1 -> _R1
| _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
;;
PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
~continuations:[tac_use h1;
- Ring.id_tac] ~status
-
- (*tac_zero_inf_pos (rational_to_fraction c1)] ~status*)
+ tac_zero_inf_pos (rational_to_fraction c1)] ~status
)
else
)
~continuations:[!tac1;tac_use h;
- Ring.id_tac
- (*tac_zero_inf_pos
- (rational_to_fraction c)*)
+ tac_zero_inf_pos (rational_to_fraction c)
]))
)