### Sequences of values

[
  Funcon length
  Funcon index
  Funcon is-in
  Funcon first
  Funcon second
  Funcon third
  Funcon first-n
  Funcon drop-first-n
  Funcon reverse
  Funcon n-of
  Funcon intersperse
]

/*
  Sequences of two or more values are not themselves values, nor is the empty
  sequence a value. However, sequences can be provided to funcons as arguments,
  and returned as results. Many operations on composite values can be expressed
  by extracting their components as sequences, operating on the sequences, then
  forming the required composite values from the resulting sequences.
  
  A sequence with elements `X1`, ..., `Xn` is written `X1,...,Xn`.
  A sequence with a single element `X` is identified with (and written) `X`.
  An empty sequence is indicated by the absence of a term.
  Any sequence `X*` can be enclosed in parentheses `(X*)`, e.g.:
  `( )`, `(1)`, `(1,2,3)`. Superfluous commas are ignored.
  
  The elements of a type sequence `T1,...,Tn` are the value sequences `V1,...,Vn`
  where `V1:T1`, ..., `Vn:Tn`. The only element of the empty type sequence `( )`
  is the empty value sequence `( )`.
  
  `(T)^N` is equivalent to `T,...,T` with `N` occurrences of `T`.
  `(T)*` is equivalent to the union of all `(T)^N` for `N`>=0,
  `(T)+` is equivalent to the union of all `(T)^N` for `N`>=1, and
  `(T)?` is equivalent to `T | ( )`.
  The parentheses around `T` above can be omitted when they are not needed for
  disambiguation.
    
  (Non-trivial) sequence types are not values, so not included in `types`.
*/


Meta-variables 
  T, T' <: values


Funcon
  length(_:values*) : =>natural-numbers
/*
  `length(V*)` gives the number of elements in `V*`.
*/
Rule
  length( ) ~> 0
Rule
  length(V:values, V*:values*) ~> natural-successor(length(V*))


Funcon
  is-in(_:values, _:values*) : =>booleans
Rule
  is-in(V:values ,V':values, V*:values*) ~> or(is-equal(V, V'), is-in(V, V*))
Rule
  is-in(V:values, ( )) ~> false


#### Sequence indexing

Funcon
  index(_:natural-numbers, _:values*) : =>values? 
/*
  `index(N, V*)` gives the `N`th element of `V*`, if it exists, otherwise `( )`.
*/
Rule
  index(1, V:values, V*:values*) ~> V
Rule
  natural-predecessor(N) ~> N'
  -----------------------------------------------------------------
  index(N:positive-integers, _:values, V*:values*) ~> index(N', V*)
Rule
  index(0, V*:values*) ~> ( )
Rule
  index(_:positive-integers, ( )) ~> ( )


/* Total indexing funcons: */

Funcon 
  first(_:T, _:values*) : =>T
Rule
  first(V:T, V*:values*) ~> V

Funcon 
  second(_:values, _:T, _:values*) : =>T
Rule
  second(_:values, V:T, V*:values*) ~> V

Funcon 
  third(_:values, _:values, _:T, _:values*) : =>T
Rule
  third(_:values, _:values, V:T, V*:values*) ~> V


#### Homogeneous sequences


Funcon
  first-n(_:natural-numbers, _:(T)*) : =>(T)*
Rule
  first-n(0, V*:(T)*) ~> ( )
Rule
  natural-predecessor(N) ~> N'
  -----------------------------------------------------------------
  first-n(N:positive-integers, V:T, V*:(T)*) ~> (V,first-n(N', V*))
Rule
  first-n(N:positive-integers, ( )) ~> ( )


Funcon
  drop-first-n(_:natural-numbers, _:(T)*) : =>(T)*
Rule
  drop-first-n(0, V*:(T)*) ~> V*
Rule
  natural-predecessor(N) ~> N'
  -----------------------------------------------------------------------
  drop-first-n(N:positive-integers, _:T, V*:(T)*) ~> drop-first-n(N', V*)
Rule
  drop-first-n(N:positive-integers, ( )) ~> ( )


Funcon
  reverse(_:(T)*) : =>(T)*
Rule
  reverse( ) ~> ( )
Rule
  reverse(V:T, V*:(T)*) ~> (reverse(V*), V)


Funcon
  n-of(N:natural-numbers, V:T) : =>(T)*
Rule
  n-of(0, _:T) ~> ( )
Rule
  natural-predecessor(N) ~> N'
  --------------------------------------------------
  n-of(N:positive-integers, V:T) ~> (V, n-of(N', V))


Funcon
  intersperse(_:T', _:(T)*) : =>(T, (T', T)*)?
Rule
  intersperse(_:T', ( )) ~> ( )
Rule
  intersperse(_:T', V) ~> V
Rule
  intersperse(V':T', V1:T, V2:T, V*:(T)*) ~> (V1, V', intersperse(V', V2, V*))