... ==
case x
of inl(x) => loc[x]
| inr(x) => case x
of inl(x) => loc_tag[fst(x); snd(x)]
| inr(x) => case x
of inl(x) => guards[fst(x); snd(x)]
| inr(x) => case x
of inl(x) => msg[fst(x); snd(x)]
| inr(x) => case x
of inl(x) => fire
| inr(x) => ...
Definitions :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
pi1: fst(t),
pi2: snd(t)
FDL editor aliases :
PiDataVal_ind
PiDataVal_ind
... ==
case x
of inl(x) => loc[x]
| inr(x) => case x
of inl(x) => loc$_{tag}$[fst(x); snd(x)]
| inr(x) => case x
of inl(x) => guards[fst(x); snd(x)]
| inr(x) => case x
of inl(x) => msg[fst(x); snd(x)]
| inr(x) => case x
of inl(x) => fire
| inr(x) => case x
of inl(x) => continue
| inr(x) => case x
of inl(x) => ...
| inr(x) => ...
Date html generated:
2010_08_27-PM-08_42_54
Last ObjectModification:
2010_04_23-AM-11_31_32
Home
Index