Zulip Chat Archive

Stream: new members

Topic: inductive datatype error


view this post on Zulip Michael Hahn (Jul 17 2020 at 00:50):

Hello,
I'm currently getting an error about inductive types that I don't quite understand:

structure simple_graph :=
(E: V → V → Prop)
(loopless: irreflexive E)
(undirected: symmetric E)


inductive path [G : simple_graph V]: V → V → Type*
| nil  : Π (h : V), path h h
| cons : Π {h s t : V} (e : G.E h s) (l : path s t), path h t

Error:

universe level of type_of(arg #3) of 'path.nil' is too big for the corresponding inductive datatype

view this post on Zulip Bryan Gin-ge Chen (Jul 17 2020 at 00:58):

This works:

universes u
variable (V : Type u)

structure simple_graph :=
(E: V  V  Prop)
(loopless: irreflexive E)
(undirected: symmetric E)


inductive path [G : simple_graph V]: V  V  Type u
| nil  : Π (h : V), path h h
| cons : Π {h s t : V} (e : G.E h s) (l : path s t), path h t

I think the universe assigned to the Type* in path has to be greater than or equal to the universe level that V lives in?

view this post on Zulip Michael Hahn (Jul 17 2020 at 01:18):

Thank you!


Last updated: May 11 2021 at 00:31 UTC