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