---

compileE#Rule(env;erl) ==
  let exp,A,parms = erl in 
  let wf,dvs = esharp-expr(env;exp) in
    <wf  (A = hd(cdv-types(hd(dvs)))), Meaning(<hd(dvs), parms>)>

---

Definitions :  spreadn: spread3,  spread: spread def,  esharp-expr: esharp-expr(env;x),  and: P  Q,  equal: s = t,  universe: Type,  cdv-types: cdv-types(dv),  prop-rule-meaning: Meaning(pr),  pair: <a, b>,  hd: hd(l)
FDL editor aliases :  compile-esharp-rule

---

compileE\#Rule(env;erl)  ==
    let  exp,A,parms  =  erl  in 
    let  wf,dvs  =  esharp-expr(env;exp)  in
        <wf  \mwedge{}  (A  =  hd(cdv-types(hd(dvs)))),  Meaning(<hd(dvs),  parms>)>


Date html generated: 2010_08_27-PM-08_22_44
Last ObjectModification: 2010_06_23-PM-04_09_22

Home Index