a stack?

Stream: Is there code for X?

[JJ]

Is there a standard last-in first-out data structure in the standard library?

[Kim Morrison]

List? :-)

[JJ]

Ha, maybe :-D

I would need a way to index backwards into it. Unfortunately, Loogling List ?a -> Nat -> Option ?a only finds List.get?. I can't just do foo[foo.length - n - 1]on account of subtraction bottoming out at zero.

Is there any nice notation for this, like foo[^idx] or the like? My peek? function is currently very ugly, lol.

[JJ]

namespace Array
def peekn? (env : Array α) n :=
  if n >= env.size then none else env[env.size - n - 1]?
notation array "[^" n "]?" => Array.peekn? array n
end Array

#eval #[1, 2, 3][^0]? -- some 3

I guess that's not bad!

[Anthony Fernandes]

Does you application really need backward indexing? If no, something like this do the trick (maybe with Stack as a structure to provide a bit more separation between it and List)

abbrev Stack := List

namespace Stack

variable {α : Type}

def empty : Stack α := []

def of_list : List α → Stack α := id

def push (x : α) (s : Stack α) : Stack α := x :: s

def pop? : Stack α → Option α × Stack α
| [] => (none, [])
| x :: xs => (x, xs)

def peek? (s : Stack α) : Option α := s[0]?

def is_empty (s : Stack α) : Prop := s = []

end Stack