must live in same universe

Stream: general

[Reid Barton]

Any insight into this error?

inductive value
| object : rbmap string value → value
/-
nested inductive type compiled to invalid inductive type
nested exception message:
nested inductive type compiled to invalid inductive type
nested exception message:
nested inductive type compiled to invalid inductive type
nested exception message:
nested occurrence 'rbnode.well_formed.{0} _nest_3_3.prod.json.value (fun (a : _nest_3_3.prod.json.value) (b : _nest_3_3.prod.json.value), (has_lt.lt.{0} string string.has_lt (prod.fst.{0 0} string _nest_3_3.json.value a) (prod.fst.{0 0} string _nest_3_3.json.value b)))' lives in universe '0' but must live in the same universe as the inductive types being declared, which is '1'
-/

[Reid Barton]

I think it's because rbtree is defined as a subtype, and so contains a field which is a Prop, but I don't know what I should do about it

[Simon Hudon]

You can only use inductive types this way. rbnode is inductive so you may be able to write your definition as:

inductive value
| object : forall (t : rbnode /- something in terms of value -/), t.well_formed lt -> value

[Simon Hudon]

Then you can write a function that puts the rbmap back together.

[Mario Carneiro]

You can define it if you use meta inductive

[Reid Barton]

Oh nice, meta is good enough for me (for now anyways)