- 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 HelmLibraryObjects.Reals.rplus_SURI))
+ :: List.map acic2cexpr args)
+ in
+ let rec aux acc = function
+ | [ Cic.AConst (nid, uri, []); n] when
+ UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
+ (match n with
+ | Cic.AConst (_, uri, []) when
+ UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
+ Num (Some aid, string_of_int (acc + 2))
+ | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
+ UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
+ aux (acc + 1) args
+ | _ -> appl ())
+ | _ -> appl ()
+ in
+ aux 0 args)
+;;
+
+(* zero and one *)
+
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
+ (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
+
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
+ (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;