Nuprl Definition : zip

zip(as;bs) ==
  fix((λzip,as,bs. case as of [] => [] | a::as' => case bs of [] => [] | b::bs' => [<a, b> / (zip as' bs')] esac esac)) \000Cas bs


Definitions occuring in Statement :  list_ind: list_ind,  cons: [a / b],  nil: [],  apply: f a,  fix: fix(F),  lambda: λx.A[x],  pair: <a, b>
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  list_ind: list_ind,  nil: [],  cons: [a / b],  pair: <a, b>,  apply: f a
FDL editor aliases :  zip
Latex:
zip(as;bs)  ==
    fix((\mlambda{}zip,as,bs.  case  as  of 
                                          []  =>  [] 
                                          a::as'  =>
                                            case  bs  of  []  =>  []  |  b::bs'  =>  [<a,  b>  /  (zip  as'  bs')]  esac 
                                    esac)) 
    as 
    bs


Date html generated: 2016_05_14-PM-03_13_23
Last ObjectModification: 2015_09_22-PM-05_58_51

Theory : list_1


Home Index