st-similar(st1;st2) ==
case(st1)
var(v)=>
st2.(st_var?(st2) 
st_var-name(st2) =a v)
const(t)=>st2.st_const?(st2)
a
b =>ra,rb.st2.(st_arrow?(st2)
(ra st_arrow-domain(st2))
(rb st_arrow-range(st2)))
a 
b =>ra,rb.st2.(st_prod?(st2)
(ra st_prod-fst(st2))
(rb st_prod-snd(st2)))
a + b =>ra,rb.st2.(st_union?(st2)
(ra st_union-left(st2))
(rb st_union-right(st2)))
a list =>ra.st2.(st_list?(st2) (ra st_list-kind(st2)))
Class(a) =>ra.st2.(st_class?(st2) (ra st_class-kind(st2)))
st2
Definitions occuring in Statement :
st_class-kind: st_class-kind(x),
st_class?: st_class?(x),
st_list-kind: st_list-kind(x),
st_list?: st_list?(x),
st_union-right: st_union-right(x),
st_union-left: st_union-left(x),
st_union?: st_union?(x),
st_prod-snd: st_prod-snd(x),
st_prod-fst: st_prod-fst(x),
st_prod?: st_prod?(x),
st_arrow-range: st_arrow-range(x),
st_arrow-domain: st_arrow-domain(x),
st_arrow?: st_arrow?(x),
st_const?: st_const?(x),
st_var-name: st_var-name(x),
st_var?: st_var?(x),
simple_type_ind: simple_type_ind,
eq_atom: x =a y,
band: p q,
apply: f a,
lambda: x.A[x]
Definitions :
simple_type_ind: simple_type_ind,
st_var?: st_var?(x),
eq_atom: x =a y,
st_var-name: st_var-name(x),
st_const?: st_const?(x),
st_arrow?: st_arrow?(x),
st_arrow-domain: st_arrow-domain(x),
st_arrow-range: st_arrow-range(x),
st_prod?: st_prod?(x),
st_prod-fst: st_prod-fst(x),
st_prod-snd: st_prod-snd(x),
st_union?: st_union?(x),
st_union-left: st_union-left(x),
st_union-right: st_union-right(x),
st_list?: st_list?(x),
st_list-kind: st_list-kind(x),
lambda: x.A[x],
band: p q,
st_class?: st_class?(x),
apply: f a,
st_class-kind: st_class-kind(x)
FDL editor aliases :
st-similar
st-similar(st1;st2) ==
case(st1)
var(v)=>\mlambda{}st2.(st\_var?(st2) \mwedge{}\msubb{} st\_var-name(st2) =a v)
const(t)=>\mlambda{}st2.st\_const?(st2)
a{}\mrightarrow{}b =>ra,rb.\mlambda{}st2.(st\_arrow?(st2) \mwedge{}\msubb{} (ra st\_arrow-domain(st2)) \mwedge{}\msubb{} (rb st\_arrow-range(st2)))
a \mtimes{} b =>ra,rb.\mlambda{}st2.(st\_prod?(st2) \mwedge{}\msubb{} (ra st\_prod-fst(st2)) \mwedge{}\msubb{} (rb st\_prod-snd(st2)))
a + b =>ra,rb.\mlambda{}st2.(st\_union?(st2) \mwedge{}\msubb{} (ra st\_union-left(st2)) \mwedge{}\msubb{} (rb st\_union-right(st2)))
a list =>ra.\mlambda{}st2.(st\_list?(st2) \mwedge{}\msubb{} (ra st\_list-kind(st2)))
Class(a) =>ra.\mlambda{}st2.(st\_class?(st2) \mwedge{}\msubb{} (ra st\_class-kind(st2)))
st2
Date html generated:
2011_08_17-PM-04_54_43
Last ObjectModification:
2011_02_07-PM-04_01_22
Home
Index