Zulip Chat Archive

Stream: lean4

Topic: mark variable as outParam


Jon Eugster (Jan 22 2025 at 10:20):

Is there a way to mark a variable as outParam similar to how variable (V) in makes it explicit? I assume not because outParam seems to be a plain definition, but I thought I'd ask.

The issue is that I have the following variable declaration:

variable {J : Type u₁} [Category.{v₁} J] {K : Type u₂} [Category.{v₂} K]
variable (V : Type u') [Category.{v'} V] [MonoidalCategory V]
variable {C : Type u} [Category.{v} C] [EnrichedOrdinaryCategory V C]
variable (F : J  C) (c : Cone F)

and for one single class in the file, I need (V : outParam <| Type u') instead. So now I have to write

variable (V : outParam <| Type u') [Category.{v'} V] [MonoidalCategory V] in
variable {C : Type u} [Category.{v} C] [EnrichedOrdinaryCategory V C] (F : J  C) in
class ...

instead of something nice like, idk

variable (outParam V) in
class ...

Last updated: May 02 2025 at 03:31 UTC