search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.65k stars 418 forks source link

Suggestion on Document: Explicit Declaration for Multiple Universe Level Variable #4122

Open DKXXXL opened 5 months ago

DKXXXL commented 5 months ago

Hello Lean Developer,

I was writing universe-lifting function due to lack of cumulative universe

inductive  liftU.{u v}  (X: Type u) : Type (max v (u + 1)) := 
  | inh : X → liftU X

It doesn't work, and I was stuck on the document for a while, not sure if explicit universe-level variable declaration can be done.

Then my friend told me I have to add a comma between u and v for multiple variables. Problem solved.

I think document it would be of great help.

When I was trying all sorts of syntax, I bump into the following seemingly working.

inductive LiftU {u : Type x} {v : Type y} (X : Type u) : Type (max v (u + 1)) :=
  | inh : X → LiftU X

I wonder if this is an intended behaviour (i.e. universe level type is some Type _). Also wonder if the above level x y for the level u v would impact anything.

I believe documenting these would be of great help for the Lean beginner, great thanks!

kim-em commented 5 months ago

@david-christiansen, this is a FPIL request, I guess, so I'll let you file it away?

kim-em commented 5 months ago

@DKXXXL, if you look up ULift, you will find this already exists, and there is quite a bit of API for it in Mathlib.

david-christiansen commented 5 months ago

I'd say this goes in the reference manual, not FPiL, but I'm the right one to assign!