Default argument depending on type

Stream: new members

[Josh Cohen]

I am trying to define something like the following:

inductive Foo (T : Type := Unit) : Type where
| A
| B (t : T) (f: Foo T)

I would like the t argument to Bto be automatically populated with () whenever T is Unit (or even just in the default case). Is this possible?

[Kenny Lau]

inductive Foo (T : Type := Unit) : Type where
| A
| B (t : T := by exact ()) (f: Foo T)

[Robin Arnez]

Just to note though: Default arguments before mandatory arguments don't make much sense (unless you're willing to write (Foo.B) .A)

[Josh Cohen]

Thanks, yes I figured out that I needed to move the default argument to the end