From 745172f5539ce7ed456c3924e13f4f0c1df9437d Mon Sep 17 00:00:00 2001 From: Louis Date: Wed, 11 Oct 2023 11:33:06 +0200 Subject: [PATCH] vault backup: 2023-10-11 11:33:06 --- Algo/CM/Lists.md | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/Algo/CM/Lists.md b/Algo/CM/Lists.md index 37ce20f..2bfebcf 100644 --- a/Algo/CM/Lists.md +++ b/Algo/CM/Lists.md @@ -14,7 +14,7 @@ USES OPERATIONS emptylist : -> list (* Internal operations of list*) - cons : list x element -> list (* Internal operations of list *) + cons : element x list -> list (* Internal operations of list *) tail : list -> list (* Internal operations of list *) head : list -> box (* Internal operations of box *) contents : box -> element (* Observer of box *) @@ -22,17 +22,17 @@ OPERATIONS next : box -> box (* Internal operation of box *) PRECONDITIONS - tail(_l_) is-defined-iaoi _l_ ≠ emptylist - head(_l_) is-defined-iaoi _l_ ≠ emptylist - first(_l_) is-defined-iaoi _l_ ≠ emptylist + tail(l) is-defined-iaoi l ≠ emptylist + head(l) is-defined-iaoi l ≠ emptylist + first(l) is-defined-iaoi l ≠ emptylist AXIOMS - first(_l_) = contents(head(_l_)) - tail(cons(_e,l_)) = _l_ - first(cons(_e,l_)) = _e_ - next(head(_l_)) = head(tail(_l_)) + first(_l_) = contents(head(l)) + tail(cons(_e,l_)) = l + first(cons(_e,l_)) = e + next(head(_l_)) = head(tail(l)) WITH - list _l_ - element _e_ + list l + element e ```