I would like to know if it is possible/easy to encode the generalization function/relation in Abella.
For Hindley-Milner, the generalization relation states like: if G |- e : t, a \not\in free(G), then G |- e : \forall a. t
Correct me if I am wrong, we need to
1. collect the set(list) of free variables in t, which is basically a traversal through the structure of types, where duplicated variable names should be taken good care
2. "generalize" t through Abella's HOAS, say, gen (var a :: fvs) (t a) r := gen fvs (all t) r
But the approach I thought seems complicated (or quite algorithmic), and I would like to know if any other encodings may look better.
Or is it common to encode the generalization relation abstractly? (Something like the HM declarative generalization relation stated above) And how?
Thanks anyway for your attention and help!