Encoding CIC in XML: terms and objects
In CIC we have (lambda)terms, objects, sections.
Lambda terms never occur alone (would have no meaning),
but only inside objects ===> markup for terms will be nested inside markup
for objects
Objects, instead, are autonomous entities, completely
identified in Coq by a name and a Section Path ===> every object is
exported to a file whose name is the name of the object. The files
are structured in directories, one for each Coq section, so that the
path of the XML file becomes the Section Path of the Coq object
In Coq theories are developed in ".v" files.
Each file is thought as a (root) homonymous section. Usually,
".v" files are further structured into directories, but this
information is lost in Coq. Instead, we think that this is important
===> directories in which ".v" files reside are mapped
into sections. This is a snapshot of
the structure of the exported Coq standard library