Zulip Chat Archive

Stream: general

Topic: more lean incompleteness

view this post on Zulip Mario Carneiro (Apr 04 2018 at 05:17):

@Gabriel Ebner I found another place where I lie in the paper compared to lean's actual behavior:

universe u
inductive fooProp : Prop | mk : ℕ → fooProp --ok
inductive fooType : Type u | mk : ℕ → fooType --ok
inductive fooSort : Sort u | mk : ℕ → fooSort
-- universe level of type_of(arg #1) of 'foo.mk' is too big for the corresponding inductive datatype

I assumed the last definition should work, writing the universe constraint as imax v u <= u where u is the sort of the inductive type itself (here u) and v is the sort of the constructor argument (here 1). Is this just because lean doesn't know how to prove imax 1 u <= u?

Last updated: May 11 2021 at 23:11 UTC