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