Funcons-beta : Tuples.cbs | PRETTY | PDF

Tuples

[
  Datatype tuples
  Funcon   tuple-elements
  Funcon   tuple-zip
]

Meta-variables
  T1, T2 <: values
  T1+, T2+ <: values+
  T*, T1*, T2* <: values*

Datatype 
  tuples(T*) ::= tuple(_:T*)

T* can be any sequence of types, including ( ) and values*.

The values of type tuples(T_1, ..., T_n) are of the form tuple(V_1, ..., V_n) with V_1:T_1, …, V_n:T_n.

Funcon
  tuple-elements(_:tuples(T*)) : =>(T*)
Rule
  tuple-elements(tuple(V*:T*)) ~> V*

Funcon
  tuple-zip(_:tuples(values*), _:tuples(values*)) : =>(tuples(values,values))*

tuple-zip(TV1, TV2) takes two tuples, and returns the sequence of pairs of their elements, provided that they have the same length. If they have different lengths, the last elements of the longer sequence are ignored.

Rule
  tuple-zip(tuple(V1:T1, V1*:T1*), tuple(V2:T2, V2*:T2*))
   ~> (tuple(V1, V2), tuple-zip(tuple(V1*), tuple(V2*)))
Rule
  tuple-zip(tuple( ), tuple( )) ~> ( )
Rule
  tuple-zip(tuple(V1+:T1+), tuple( )) ~> ( )
Rule
  tuple-zip(tuple( ), tuple(V2+:T2+)) ~> ( )

← ↑ →