Nuprl Definition : list-deq

list-deq(eq) ==
  λas,bs. (rec-case(as) of
           [] => λL.null(L)
           a::as' =>
            r.λL.rec-case(L) of
                 [] => ff
                 b::bs' =>
                  r2.(eq a b) ∧b (r bs') 
           bs)


Definitions occuring in Statement :  null: null(as),  list_ind: list_ind,  band: p ∧b q,  bfalse: ff,  apply: f a,  lambda: λx.A[x]
Definitions occuring in definition :  null: null(as),  lambda: λx.A[x],  list_ind: list_ind,  bfalse: ff,  band: p ∧b q,  apply: f a
FDL editor aliases :  list-deq
Latex:
list-deq(eq)  ==
    \mlambda{}as,bs.  (rec-case(as)  of
                      []  =>  \mlambda{}L.null(L)
                      a::as'  =>
                        r.\mlambda{}L.rec-case(L)  of
                                  []  =>  ff
                                  b::bs'  =>
                                    r2.(eq  a  b)  \mwedge{}\msubb{}  (r  bs') 
                      bs)


Date html generated: 2016_05_14-AM-06_55_06
Last ObjectModification: 2015_12_23-PM-08_19_52

Theory : list_0


Home Index