Is there a way to define the "real" version of a struct?

Stream: general

[Srayan Jana]

From what I understand, the way Lean handles stuff like Lists is that some of them are actually arrays for performance related reasons, but are treated like linked lists in order to make the logic model work. And, correct me if I'm wrong, this is true for some other stuff like numbers.

Is there a way for a Lean developer to be able to set the "real" world version of the struct as well as the logic version?

[Srayan Jana]

I think this thread is where I got the idea from: #lean4 dev > Unboxed structure types

[Aaron Liu]

I think lists are actually lists?

[Srayan Jana]

I swear I read somewhere about how behind the scenes, Lean optimizes away linked lists into arrays, but don't quote me on that

[Srayan Jana]

@Aaron Liu https://lean-lang.org/doc/reference/latest/Basic-Types/Strings/
specifically for Strings, in the Lean programming model, they're treated as Linked Lists, but in the actual runtime, they're treated as Arrays

[Aaron Liu]

Srayan Jana said:

I swear I read somewhere about how behind the scenes, Lean optimizes away linked lists into arrays, but don't quote me on that

I think lists are lists and arrays are arrays, even though arrays are defined as a wrapper around lists

[David Ledvinka]

I think maybe you are confusing it with the fact that Arrays are treated as lists in the logical model but compile to dynamic arrays. So you prove things about array operations as if it were a linked list.

[Srayan Jana]

Ah, that makes more sense, thank you!