- Appl
- (Some aid, (Symbol (Some sid, "plus",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
- :: List.map acic2cexpr args));;
+ let appl () =
+ Appl
+ (Some aid, (Symbol (Some sid, "plus",
+ None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
+ :: List.map acic2cexpr args)
+ in
+ let rec aux acc = function
+ | [ Cic.AConst (nid, uri, []); n] when
+ UriManager.eq uri r1_uri ->
+ (match n with
+ | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
+ Num (Some aid, string_of_int (acc + 2))
+ | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
+ UriManager.eq uri rplus_uri ->
+ aux (acc + 1) args
+ | _ -> appl ())
+ | _ -> appl ()
+ in
+ aux 0 args)
+;;
+
+(* zero and one *)
+
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con"
+ (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
+
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con"
+ (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;