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