Nuprl Definition : lapp_imon
<T List,@> == <T List, λx,y. tt, λx,y. tt, λx,y. (x @ y), [], λx.x>
Definitions occuring in Statement :
append: as @ bs,
nil: [],
list: T List,
btrue: tt,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
list: T List,
btrue: tt,
append: as @ bs,
pair: <a, b>,
nil: [],
lambda: λx.A[x]
Latex:
<T List,@> == <T List, \mlambda{}x,y. tt, \mlambda{}x,y. tt, \mlambda{}x,y. (x @ y), [], \mlambda{}x.x>
Date html generated:
2016_05_16-AM-07_37_43
Last ObjectModification:
2015_09_23-AM-09_51_33
Theory : list_2
Home
Index