dependence for default structure arguments?

Stream: lean4

[Siddharth Bhat]

What are the semantics of default arguments in Lean? I would like if something like this:

structure MWE where
  motive: Nat → Type := Fin
  val : motive 1 := Fin.ofNat 0

succeeds, but I can understand if the semantics of default arguments is that the default arguments should not "depend" on one another.

[Kyle Miller]

One trick you can use is to use a tactic instead, which is allowed to fail:

structure MWE where
  motive: Nat → Type := Fin
  val : motive 1 := by exact 0

I'm not sure why you can't do by exact Fin.ofNat 0 here. ("invalid auto tactic, identifier is not allowed")

[Kyle Miller]

This doesn't completely work because there's no OfNat (motive 1) 0 instance, but this works at least as a proof-of-concept:

def a := MWE.mk Fin

[Kyle Miller]

I would have thought that default arguments show up as optional arguments to the constructor, but it seems not. This works at least:

macro "try_zero" : tactic => `(tactic| exact Fin.ofNat 0)

structure MWE where
  motive: Nat → Type := Fin
  val : motive 1 := by try_zero

def a : MWE := {}