Stacks push and pop

Stream: new members

[Omar Hidmi]

Hi everyone .. I'm totally new to LEAN and I started studying this language and trying to prove things, started by finishing some levels in Natural Number Game and also learning LEAN from the documentation, but now I have a task to do with Stacks, I have to create a Stack A and Stack B and then I push items to Stack A and pop them to Stack B to prove the last item remaining on top of Stack A ... can you point me to the right direction ?????
Thanks a ton

[Patrick Massot]

Welcome! Please read the explanation at #mwe to learn how to ask more efficient questions.

[Omar Hidmi]

to be clear .. I am asking about Stacks .. is it the same as Arrays or Lists ? or there is pre-defined structure in LEAN for Stacks ? I wanted someone to guide me to the right direction

[Johan Commelin]

@Omar Hidmi You can just use a lists.

[Adam Topaz]

Lean4 has docs4#Std.Stack

[Adam Topaz]

And you can see that it's defined in terms of arrays

[Adam Topaz]

if you click that link and look around you will see all the relevant API (pop, push, etc.)

[Adam Topaz]

I guess we should ask @Omar Hidmi whether you want to use Lean3 or Lean4?

[Omar Hidmi]

Thanks @Adam Topaz That's exactly what I needed .. thanks