referring to fields in `extends`

Stream: new members

[Alok Singh]

structure NonEmptyArray (α : Type) extends Array α where
  h : ?.size > 0 -- I want to refer to the data field of the array
  deriving Repr

How could I fill in the ??

I could write it like

structure NonEmptyArray (α : Type) where
  /-- The underlying array data -/
  data : Array α
  /-- Proof that the array is non-empty -/
  h : data.size > 0
  deriving Repr

but I'm curious how to do it with extends.

[Kyle Miller]

structure NonEmptyArray (α : Type) extends Array α where
  h : toArray.size > 0
  deriving Repr

You can see "toArray" in the Expected Type window.

[Kyle Miller]

If you want it to be data, you can do

structure NonEmptyArray (α : Type) extends data : Array α where
  h : data.size > 0
  deriving Repr

[Kyle Miller]

I'm not sure if it will have any of the runtime semantics of an Array. It might, because NonEmptyArray.mk shows it has an Array as the first argument.