---

esharp-expr(env;x) ==
  case(x)
  leaf(F) => <esharp-base-wf(env;F), [esharp-base(env;F)]>
  pair(a,b) => ra,rb.let wf1,L1 = ra in
                       let wf2,L2 = rb in
                         <wf1  wf2, L1 @ L2>
  F(a) => ra.let wf,L = ra in
               <wf  esharp-comb-wf(env;F;L), [esharp-comb(env;F;L)]>

---

Definitions :  expression_ind: expression_ind,  assert: b,  esharp-base-wf: esharp-base-wf(env;x),  esharp-base: esharp-base(env;x),  append: as @ bs,  spread: spread def,  pair: <a, b>,  and: P  Q,  esharp-comb-wf: esharp-comb-wf(env;F;ra),  cons: [car / cdr],  esharp-comb: esharp-comb(env;F;ra),  nil: []
FDL editor aliases :  esharp-expr

---

esharp-expr(env;x)  ==
    case(x)
    leaf(F)  =>  <\muparrow{}esharp-base-wf(env;F),  [esharp-base(env;F)]>
    pair(a,b)  =>  ra,rb.let  wf1,L1  =  ra  in
                                              let  wf2,L2  =  rb  in
                                                  <wf1  \mwedge{}  wf2,  L1  @  L2>
    F(a)  =>  ra.let  wf,L  =  ra  in
                              <wf  \mwedge{}  esharp-comb-wf(env;F;L),  [esharp-comb(env;F;L)]>


Date html generated: 2010_08_27-PM-08_22_10
Last ObjectModification: 2010_06_22-PM-05_58_55

Home Index