Nuprl Definition : ecl_ind_ecland_compseq_tag_def 11,40
ecl_ind_ecland{ecl ind ecland compseq tag def:ObjectId}
ecl_ind_ecland(v11,v12,v13.catch(v11;v12;v13);
ecl_ind_ecland(v21,v22,v23.throw(v21;v22;v23);
ecl_ind_ecland(v31,v32,v33.act(v31;v32;v33);
ecl_ind_ecland(v41,v42.repeat(v41;v42);
ecl_ind_ecland(v51,v52,v53,v54.or(v51;v52;v53;v54);
ecl_ind_ecland(v61,v62,v63,v64.and(v61;v62;v63;v64);
ecl_ind_ecland(v71,v72,v73,v74.seq(v71;v72;v73;v74);
ecl_ind_ecland(v81,v82.base(v81;v82);
ecl_ind_ecland(b;
ecl_ind_ecland(a)
== compseq(ecl_ind(ecland(a; b);
== compseq(ecl_ind(k,test.base(k;test);
== compseq(ecl_ind(a,b,rec1,rec2.seq(a;b;rec1;rec2);
== compseq(ecl_ind(a,b,rec1,rec2.and(a;b;rec1;rec2);
== compseq(ecl_ind(a,b,rec1,rec2.or(a;b;rec1;rec2);
== compseq(ecl_ind(a,rec1.repeat(a;rec1);
== compseq(ecl_ind(a,n,rec1.act(a;n;rec1);
== compseq(ecl_ind(a,n,rec1.throw(a;n;rec1);
== compseq(ecl_ind(a,l,rec1.catch(a;l;rec1));
== compseq(and(a
== compseq(and;b
== compseq(and;ecl_ind(a;
== compseq(and;ecl_ind(k,test.base(k;test);
== compseq(and;ecl_ind(a,b,rec1,rec2.seq(a;b;rec1;rec2);
== compseq(and;ecl_ind(a,b,rec1,rec2.and(a;b;rec1;rec2);
== compseq(and;ecl_ind(a,b,rec1,rec2.or(a;b;rec1;rec2);
== compseq(and;ecl_ind(a,rec1.repeat(a;rec1);
== compseq(and;ecl_ind(a,n,rec1.act(a;n;rec1);
== compseq(and;ecl_ind(a,n,rec1.throw(a;n;rec1);
== compseq(and;ecl_ind(a,l,rec1.catch(a;l;rec1))
== compseq(and;ecl_ind(b;
== compseq(and;ecl_ind(k,test.base(k;test);
== compseq(and;ecl_ind(a,b,rec1,rec2.seq(a;b;rec1;rec2);
== compseq(and;ecl_ind(a,b,rec1,rec2.and(a;b;rec1;rec2);
== compseq(and;ecl_ind(a,b,rec1,rec2.or(a;b;rec1;rec2);
== compseq(and;ecl_ind(a,rec1.repeat(a;rec1);
== compseq(and;ecl_ind(a,n,rec1.act(a;n;rec1);
== compseq(and;ecl_ind(a,n,rec1.throw(a;n;rec1);
== compseq(and;ecl_ind(a,l,rec1.catch(a;l;rec1)))) 
latex

Definitionsecland(a; b), ecl ind

origin