Internally forwarders should be terms

[np]

Internally we have At for term-as-a-process and Ax for forwarders (axioms). Ideally I think Ax should disappear and become At (Def fwdName ...).

• This would remove some redundant code
• This would allow to use fwd in terms directly instead of proc(cs...) fwd ... (cs...)
• Improvements made on term-as-a-process would benefit forwarders

Now we have two forms of forwarders:

• fwd <Nat> <Session> <Channel>
• fwd <Session> ( <Channel>* )

The first form can be given a general type:

fwd : (n : Int)(S : Session) -> < Fwd n S >

The second is using a flat sequence of sessions and we cannot express this type as only Session is exposed and not [RSession].

Therefor using the first form internally seems more appropriate.

The second form would then be a consequence of a more liberal form of term-as-a-process.

Note that so far what we have internally is the reverse the first form is a wrapper around the second.