Zulip Chat Archive
Stream: lean4
Topic: OutParam
Kenny Lau (Aug 12 2025 at 12:59):
Why is outParam (α : Sort u) : Sort u lowercase?
Aaron Liu (Aug 12 2025 at 13:15):
also docs#semiOutParam docs#optParam docs#autoParam
Kenny Lau (Aug 12 2025 at 13:16):
?
Aaron Liu (Aug 12 2025 at 13:17):
lowercase
Aaron Liu (Aug 12 2025 at 13:17):
they are also lowercase
Kenny Lau (Aug 12 2025 at 13:17):
ah, I thought you were answering my question
François G. Dorais (Aug 12 2025 at 14:20):
Long ago it was out_param...
Mario Carneiro (Aug 15 2025 at 13:13):
This was on my list of renames that went nowhere lean4#1897
Last updated: Dec 20 2025 at 21:32 UTC