I would like to have things parameterized or functorized in such a way that the user can provide a signature for a language some type 'a term_f or whatever. Then, the elaboration framework can be generated from this.
Basically, I think that the concrete representation of terms (things like In and Ref constructors) should be completely internal to the elaborator, and not exposed. It's basically this way already, but it is tangled up with the actual definition of the term grammar at the moment.
I would like to have things parameterized or functorized in such a way that the user can provide a signature for a language some type
'a term_for whatever. Then, the elaboration framework can be generated from this.Basically, I think that the concrete representation of terms (things like
InandRefconstructors) should be completely internal to the elaborator, and not exposed. It's basically this way already, but it is tangled up with the actual definition of the term grammar at the moment.