OpenMath Content Dictionary: list4

Canonical URL:
http://www.openmath.org/cd/list2.ocd
CD Base:
http://www.openmath.org/cd
CD File:
list4.ocd
CD as XML Encoded OpenMath:
list4.omcd
Defines:
difference, entry, list_of_lengthn, remove, reverse
Date:
2004-11-30
Version:
5 (Revision 1)
Review Date:
2006-03-30
Status:
experimental

Several convenient but not basic list functions are given in this CD.

Arjeh M. Cohen  2004-11-30

entry

Description:

This symbol represents a binary function whose first argument should be a list L and whose second argument should be a positive integer i such that the absolute value of i is in the interval [1..n], where n is the length of L. If i is positive, it returns the i-th entry L[i] of L, if i is negative it returns the (n+1-i)-th entry of L.

Commented Mathematical property (CMP):
If i is a positive integer and a is a list of length at least i, then entry(a,i) is equal to list_selector(i,a).
Formal Mathematical property (FMP):
i > 0 entry ( a , i ) = list_selector ( i , a )
Example:
The second entry of the list [1,2,3] is 2.
entry ( ( 1 , 2 , 3 ) , 2 ) = 2
Example:
Specification of the second element of the list [1,..,6] counted from the end.
entry ( ( 1 , 2 , 3 , 4 , 5 , 6 ) , -2 ) = 5
Signatures:
sts


[Next: reverse] [Last: list_of_lengthn] [Top]

reverse

Role:
application
Description:

The reverse of a list

Formal Mathematical property (FMP):
reverse ( nil ) = nil
Formal Mathematical property (FMP):
lst , a . reverse ( cons ( a , lst ) ) = append ( reverse ( lst ) , cons ( a , nil ) )
Signatures:
sts


[Next: difference] [Previous: entry] [Top]

difference

Description:

This symbol represents a function with two arguments, both lists. When applied to two lists, it represents a list made up of all the elements of the first list which do not occur in the second, appearing in the order in which they occur in the first list.

Example:
Specification of the list [6,6,12], apart from the first 2 elements.
difference ( ( 6 , 6 , 12 ) , ( 6 ) ) = ( 12 )
Signatures:
sts


[Next: remove] [Previous: reverse] [Top]

remove

Description:

This symbol represents a function with two arguments, both lists. When applied to two lists, it represents a list made up of all the elements of the first list with those elements removed whose entries occur in the second list.

Example:
Specification of the list [6,5,6] with the second entry removed.
remove ( ( 6 , 5 , 6 ) , ( 2 ) ) = ( 6 , 6 )
Signatures:
sts


[Next: list_of_lengthn] [Previous: difference] [Top]

list_of_lengthn

Description:

This symbol represents a function with two arguments, the first of which is a natural number and the second of which is a list. The first argument is the length of the list.

Example:
A list L of length 3:
list_of_lengthn ( 3 , ( L ) )
Signatures:
sts


[First: entry] [Previous: remove] [Top]