default value of structure which is not produced by a tactic

[Seasawher]

Description

constructor of structure does not accept defalut value of field whose type is not Prop.

structure NonEmptyString where
  value : String
  another_value : Int := 0
  ev : value.length > 0 := by decide
deriving Repr

-- works
def eg : NonEmptyString := { value := "hello" }

-- does not work
def eg' : NonEmptyString := NonEmptyString.mk "hello"

-- default value of `another_value` is missing
/-
NonEmptyString.mk (value : String) (another_value : Int) (ev : value.length > 0 := by decide) : NonEmptyString
-/
#check NonEmptyString.mk

Steps to Reproduce

Expected behavior: accept defalut value for all types

Actual behavior: accept only Prop-value

Versions

nightly

Additional Information

reported on Zulip: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/default.20value.20of.20structure.20fields

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[ammkrn]

I think this is actually related to the default value being produced by a tactic, not whether the default value is Prop or Type. For example:

structure NonEmptyString where
  value : String
  another_value : Int := by exact 0
  ev : value.length > 0 := by decide
deriving Repr

-- works if `another_value` comes from a tactic
def eg' : NonEmptyString := NonEmptyString.mk "hello"

#eval eg'