Lifting should also lift datatypes about datatt HOT 4 CLOSED

It actually does lift the datatype, see my reply to your other issue. You're right that this output is confusing though.

from datatt.

Could you point me to where in the code the datatype gets lifted? I'm trying to understand your implementation. I found (in syntax.ml):

let lift i = bottom_up (function 
  | U (Const j) -> U (Const (j + i)) 
  | x -> x)

But this only lifts universes.

from datatt.

Hmmm actually yeah, datatypes in Syntax don't actually have their universe level stored syntactically. The way type lifting gets enforced on datatypes is that they have an eta-expanded version of their type constructor in their description (tm and tp in Domain.desc), and this is what actually gets lifted. I say eta-expanded but if the datatype has no parameters then tm won't be a function, of course. See what happens in Nbe.eval when evaluating a Lift. I think this is probably a pretty weird way to have implemented this haha.

from datatt.

Ah that's interesting. Definitely not how I expected it to be implemented :)

from datatt.