default value of structure fields

Stream: lean4

[Asei Inoue]

default value of structure's field must be type of Prop?

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

def eg : NonEmptyString :=
  /-
  type mismatch
    fun another_value => { value := "hello", another_value := another_value, ev := ⋯ }
  has type
    Int → NonEmptyString : Type
  but is expected to have type
    NonEmptyString : Type
  -/
  NonEmptyString.mk "hello"

[Asei Inoue]

default value of ev does work, but default value of another_valuedoes not work...

[Floris van Doorn]

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

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

works

[Asei Inoue]

why .mk function does not have default value of another_value?
is it a bug? (I think this is very surprising and it should be a bug... )

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

[Floris van Doorn]

Yeah, might be a bug.

[Asei Inoue]

ok I will submit a issue on leanprover/lean4

[Asei Inoue]

done: https://github.com/leanprover/lean4/issues/4736

[Eric Wieser]

I think default values of structure fields are different to default values of functions?

[Eric Wieser]

This also works:

inductive NonEmptyString where
  | mk
    (value : String)
    (another_value : Int := 0)
    (ev : value.length > 0 := by decide)
deriving Repr

def eg : NonEmptyString :=
  NonEmptyString.mk "hello"

[Eric Wieser]

I think defaults have to be handled specially in structure because of how they interact with inheritance

[Asei Inoue]

I think default values of structure fields are different to default values of functions?

constructor of structure should have same dafault value, I think

[Asei Inoue]

I think defaults have to be handled specially in structure because of how they interact with inheritance

oh... I hadn't thought of that ... .

[Asei Inoue]

even if this is not a bug, this is still negative surprising.

[Kyle Miller]

Default value processing for structures is rather complicated, and it only works with {...} notation

[Kyle Miller]

The main problem is that default values need to take extends into account

[Asei Inoue]

in detail, what does problem occurs if structure’s constructor have default value?

[Kyle Miller]

Here's an example:

structure A where
  x : Nat

structure B extends A where
  x := 1

#check A.mk -- A.mk (x : Nat) : A
#check B.mk -- B.mk (toA : A) : B

[Kyle Miller]

There's no place for the default value for x to go in B.mk.