Nuprl Definition : cnv-taba
cnv-taba(xs;ys) == fst(rec-case(xs) of [] => <[], ys> | x::xs' => p.let a,ys = p in let h,t = ys in <[<x, h> / a], t>)
Definitions occuring in Statement :
list_ind: list_ind,
cons: [a / b],
nil: [],
pi1: fst(t),
spread: spread def,
pair: <a, b>
Definitions occuring in definition :
pi1: fst(t),
list_ind: list_ind,
nil: [],
spread: spread def,
cons: [a / b],
pair: <a, b>
FDL editor aliases :
cnv-taba
Latex:
cnv-taba(xs;ys) == fst(rec-case(xs) of [] => <[], ys> | x::xs' => p.let a,ys = p in let h,t = ys in\000C <[<x, h> / a], t>)
Date html generated:
2016_05_15-PM-07_34_22
Last ObjectModification:
2015_09_23-AM-08_16_56
Theory : general
Home
Index