Nuprl Definition : ml_match

Nuprl Definition : ml_match_pair

ml_match_pair(e;e1,t1.p1[e1; t1];e2,t2.p2[e2; t2];t) ==
if e is a pair then let e1,e2 = e
in let b1,t1 = p1[e1; t]

                         in if b1 then p2[e2; t1] else <ff, t1> fi  otherwise <ff, t>

Definitions occuring in Statement : ifthenelse: if b then t else f fi , bfalse: ff, ispair: if z is a pair then a otherwise b, spread: spread def, pair: <a, b>
Definitions occuring in definition : ispair: if z is a pair then a otherwise b, spread: spread def, ifthenelse: if b then t else f fi , pair: <a, b>, bfalse: ff
FDL editor aliases : ml_match_pair

Latex:
ml\_match\_pair(e;e1,t1.p1[e1; t1];e2,t2.p2[e2; t2];t) == if e is a pair then let e1,e2 = e in let b1,t1 = p1[e1; t] in if b1 then p2[e2; t1] else <ff, t1> fi otherwise <ff, t> Date html generated: 2017_09_29-PM-05_50_51 Last ObjectModification: 2017_05_08-PM-04_20_06 Theory : ML Home Index