## Stream: new members

### Topic: inductive datatype error

#### 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


#### 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?

#### Michael Hahn (Jul 17 2020 at 01:18):

Thank you!

Last updated: May 11 2021 at 00:31 UTC