-val compute: body:Cic.term option -> ty:Cic.term -> MetadataTypes.metadata list
-
- (** @return tuples <uri, name, metadata> *)
-val compute_ind:
- uri:UriManager.uri -> types:Cic.inductiveType list ->
- (string * string * MetadataTypes.metadata list) list
-
-val compute_term:
- MetadataTypes.position -> Cic.term ->