Open Seasawher opened 1 month ago
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'
Description
constructor of structure does not accept defalut value of field whose type is not
Prop
.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.