let is_eq_URI uri =
List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
+let is_eq_refl_URI uri =
+ let urieq = UriManager.strip_xpointer uri in
+ is_eq_URI urieq &&
+ not (UriManager.eq urieq uri)
+;;
+
let is_eq_ind_URI uri =
List.exists (fun (_,_,_,eq_ind,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
let is_sym_eq_URI uri =
List.exists (fun (_,sym_eq,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
+let eq_refl_URI ~eq:uri =
+ let uri = UriManager.strip_xpointer uri in
+ UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)")
+
let sym_eq_URI ~eq:uri =
try
let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x