Zulip Chat Archive

Stream: lean4

Topic: How to solve the problem of universe level too big?


Erika Su (Dec 29 2022 at 06:52):

suppose i want to define a typeclass for array:

class IArray.{u, v, w} (Array : Type u -> Type v) : Type w where
 /-- some other function -/
  append            :         Append (Array β)
  assoc {β} [DecidableEq β] : {a b c : Array β} -> (a ++ b) ++ c = a ++ (b ++ c)
  -- error info of assoc : (kernel) universe level of type_of(arg #2) of 'IArray.mk' is too big for the corresponding inductive datatypeLean

Last updated: Dec 20 2023 at 11:08 UTC