Zulip Chat Archive

Stream: general

Topic: must live in same universe


Reid Barton (Jul 17 2018 at 03:04):

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 (Jul 17 2018 at 03:07):

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 (Jul 17 2018 at 03:14):

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 (Jul 17 2018 at 03:15):

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

Mario Carneiro (Jul 17 2018 at 03:15):

You can define it if you use meta inductive

Reid Barton (Jul 17 2018 at 03:16):

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


Last updated: Dec 20 2023 at 11:08 UTC