Nuprl Definition : RankEx4_ind

            RankEx4_Foo(foo) rec1.Foo[foo; rec1])  ==
  fix((λRankEx4_ind,v. let lbl,v1 
                       in if lbl="Foo"
                          then case v1 of inl(x) => Foo[inl x; Ax] inr(y) => Foo[inr RankEx4_ind y]
                          else ⊥
                          fi )) 

Definitions occuring in Statement :  bottom: atom_eq: if a=b then else fi  apply: a fix: fix(F) lambda: λx.A[x] spread: spread def decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x token: "$token" axiom: Ax
FDL editor aliases :  RankEx4_ind
                        RankEx4\_Foo(foo){}\mRightarrow{}  rec1.Foo[foo;  rec1])    ==
    fix((\mlambda{}RankEx4$_{ind}$,v.  let  lbl,v1  =  v 
                                            in  if  lbl="Foo"
                                                  then  case  v1
                                                              of  inl(x)  =>
                                                              Foo[inl  x;  Ax]
                                                              |  inr(y)  =>
                                                              Foo[inr  y  ;  RankEx4$_{ind}$  y]
                                                  else  \mbot{}
                                                  fi  )) 

Date html generated: 2015_07_17-AM-07_51_19
Last ObjectModification: 2015_01_28-PM-02_34_01

Home Index