dependent fields in structures

Stream: general

[Bhakti Shah]

Is something like

def strlt : String -> String -> Prop := (fun x x' => x < x')

structure X where
f1 : List String
f2 : List.Sorted strlt f1

a valid definition? It seems to typecheck but I suspect it's inferring the f1 within f2 to be a free variable and not the field itself.
as a follow up, is it even possible to define something where f2 is dependent on f1?

[Eric Wieser]

That does exactly what you want it to; you can confirm this with #check X.f2

[Eric Wieser]

If you're worried about free variables being introduced, turn on set_option autoImplicit false to make that never happen