Lists

[
Datatype lists
Funcon   list
Funcon   list-elements
Funcon   list-nil       Alias nil
Funcon   list-cons      Alias cons
Funcon   list-tail      Alias tail
Funcon   list-length
Funcon   list-append
]
Meta-variables
T <: values
Datatype
lists(T) ::= list(_:(T)*)

lists(T) is the type of possibly-empty finite lists [V_1,...,V_n] where V_1:T, …, V_n:T.

N.B. [T] is always a single list value, and not interpreted as the type lists(T).

The notation [V_1, ..., V_n] for list(V_1, ..., V_n) is built-in.

Assert
[V*:values*] == list(V*)
Funcon
list-elements(_:lists(T)) : =>(T)*
Rule
list-elements(list(V*:values*)) ~> V*
Funcon
list-nil : =>lists(_)
~> [ ]
Alias
nil = list-nil
Funcon
list-cons(_:T, _:lists(T)) : =>lists(T)
Alias
cons = list-cons
Rule
list-cons(V:values, [V*:values*]) ~> [V, V*]
Funcon
Alias
head = list-head
Rule
Rule
list-head[ ] ~> ( )
Funcon
list-tail(_:lists(T)) : =>(lists(T))?
Alias
tail = list-tail
Rule
list-tail[_:values, V*:values*] ~> [V*]
Rule
list-tail[ ] ~> ( )
Funcon
list-length(_:lists(T)) : =>natural-numbers
Rule
list-length[V*:values*] ~> length(V*)
Funcon
list-append(_:(lists(T))*) : =>lists(T)
Rule
list-append([V1*:values*], [V2*:values*]) ~> [V1*, V2*]
Rule
list-append(L1:lists(_), L2:lists(_), L3:lists(_), L*:(lists(_))*)
~> list-append(L1, list-append(L2, L3, L*))
Rule
list-append( ) ~> [ ]
Rule
list-append(L:lists(_)) ~> L

Datatypes of infinite and possibly-infinite lists can be specified as algebraic datatypes using abstractions.

 From the PLanCompS Project CBS-beta issues… Suggest an improvement…