Zulip Chat Archive

Stream: lean4

Topic: Syntax for constructor with explicit parameter


Horațiu Cheval (Jan 02 2023 at 11:12):

inductive Foo (n : Nat) where
| mk

#check Foo.mk
-- Foo.mk {n : Nat} : Foo n

The n parameter of Foo is an implicit argument in the mk constructor. Is there a way to say that I want it to be explicit? Other than making n an index of Foo and binding it explicitly in mk. In Lean 3 there was the [] syntax

inductive foo (n : nat)
| mk [] : foo

#check foo.mk
-- foo.mk : Π (n : ℕ), foo n

Sebastian Ullrich (Jan 02 2023 at 13:40):

Other than making n an index of Foo and binding it explicitly in mk.

There is nothing wrong with that, indices are automatically promoted to parameters where possible

Horațiu Cheval (Jan 02 2023 at 15:40):

Right, though I still prefer to write parameters before the colon, because I like how it's clear from the signature that they won't change throughout the definition, and you don't need to look at the constructors to learn that. Maybe I'm still more accustomed to Lean 3 though.


Last updated: Dec 20 2023 at 11:08 UTC