Update List/pop_back

Co-authored-by: Nicolas Abril <y906846m@anonaddy.me>
This commit is contained in:
Evan M. Matthews 2024-05-29 12:29:51 -04:00 committed by GitHub
parent 7fd6b153a2
commit 3324a53880
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194

View File

@ -111,27 +111,10 @@ List/pop_front = @l
# List pop_back:
# List l -> List l
# removes the first item from the back of list l.
List/pop_back/aux = @acc @l
match l {
List/Nil: List/Nil
List/Cons:
use x = switch acc {
0: *
_: l.head
}
use y = switch acc {
0: List/Nil
1: List/Nil
_: l.tail
}
(List/Cons x (List/pop_back/aux (- acc 1) y))
}
List/pop_back = @l
switch (- (List/len l) 1) {
0: []
_: (List/pop_back/aux (- (List/len l) 1) l)
}
# removes and discards the the last item of the list
List/pop_back (List/Nil) = List/Nil
List/pop_back (List/Cons x List/Nil) = List/Nil
List/pop_back (List/Cons head tail) = (List/Cons head (List/pop_back tail))
# List remove:
# List l -> Some s -> List l