Having a nat -> atom conversion
Opened this issue · 2 comments
since often the set of variables is assumed to be countably infinite, it's just clear that nat and atom are isomorphic types. in fact, atom is just hidden nat. would it make sense to have a function of type nat -> atom?
this would be helpful, for example,when examining a particular type checking example.
the problem here is more fundamental: Modules in Coq are opaque. that means all modules in metalib cannot compute. is there any interest to fix this problem?
Old issue, but a comment for the record: The opaqueness isn't exactly a problem. A change at this line
Module Atom : ATOM.
to
Module Atom <: ATOM.
will make the module transparent. But this comes at the cost of exposing all of its details. It would no longer be possible to distinguish between atom and nat which would, for example, totally break my own library that uses Metalib. If one wants to compute with Metalib your options are rewriting terms based on the axioms of Atom, possibly automating this with tactics (like fsetdec), or extracting to OCaml/Haskell (a quite viable option).