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