same level as

Stream: mathlib4

[Matthew Ballard]

I've found myself wanting to write Y: Type (Same level as X). I haven't seen an elaborator along those lines. Does this or something similar exist?

[Eric Wieser]

I guess it would make sense to have level_of% given we have type_of%

[Eric Wieser]

Then again, you could also just use Y : type_of% X instead of Y : Type (level_of% X)

[Eric Wieser]

My naive attempt was:

open Lean Lean.Parser in
@[term_parser] def levelOf := leading_parser
  "level_of% " >> termParser maxPrec

open Lean.Meta Lean.Elab.Term in
@[term_elab levelOf] def elabLevelOf : TermElab := fun stx _ => do
  let e ← inferType (← elabTerm stx[1] none)
  getLevel e  -- fails

but I realize now that Level is not a "term" so this probably can't be fixed

[Eric Wieser]

Maybe

builtin_initialize Lean.Parser.registerBuiltinDynamicParserAttribute `level_parser `level

in a separate file is enough to help thing move

[Mario Carneiro]

Eric Wieser said:

I guess it would make sense to have level_of% given we have type_of%

there are no macros in the level category

[Scott Morrison]

Could you give an example of what you mean that isn't (X : Type u) (Y : Type u)?

[Matthew Ballard]

Eg (X : Type*) and (Y : type_of% X)

[Eric Wieser]

I think probably explicit universes are best there

[Matthew Ballard]

How about (X1 X2 X3 ... Xn : Type*) and (Y : type_of% X37)?

[Matthew Ballard]

I had n=6 or so in "real life"

[Eric Wieser]

Is making Type* unhygienic by generating a uX37 universe variable possible and/or sane?

[Matthew Ballard]

Eh, you have kinda convinced me that it should be still be broken out