LetPairExtension.xstw

module LetPairExtension;

import PairExtension;
import LetSeqExtension;

extension {
  context-free syntax
    "(" ID "," ID ")" "=" Term -> Binding

  inductive definitions
    T-LetPair1:
      (C |- t1 : Pair T1) (C,x1:T1,x2:T1 |- let bs in t2 : T2)
      --------------------------------------------------------
      C |- let (x1,x2) = t1; bs in t2 : T2
    T-LetPair2:
      (C |- t1 : Pair T1) (C,x1:T1,x2:T1 |- t2 : T2)
      ----------------------------------------------
      C |- let (x1,x2) = t1 in t2 : T2

  desugarings
    { (C |- t1 : Pair T1) (C,x1:T1,x2:T1 |- let bs in t2 : T2)
      --------------------------------------------------------
      C |- [ let (x1,x2) = t1; bs in t2 ] : T2
      ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~>
      (\x1:T1.\x2:T1. let bs in t2) (t1.1) (t1.2) }
    { (C |- t1 : Pair T1) (C,x1:T1,x2:T1 |- t2 : T2)
      ----------------------------------------------
      C |- [ let (x1,x2) = t1 in t2 ] : T2
      ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~>
      (\x1:T1.\x2:T1. t2) (t1.1) (t1.2) }
}