Nuprl Definition : vr_BOOLDI
vr_BOOLDI == 
P:
. ((P tt) 
(P ff) (b:. (P b)))
Definitions occuring in Statement :
bfalse: ff,
btrue: tt,
bool: ,
prop: ,
all: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x]
FDL editor aliases :
vr_BOOLDI
vr\_BOOLDI == \mforall{}P:\mBbbB{} {}\mrightarrow{} \mBbbP{}. ((P tt) {}\mRightarrow{} (P ff) {}\mRightarrow{} (\mforall{}b:\mBbbB{}. (P b)))
Date html generated:
2012_02_20-PM-03_34_10
Last ObjectModification:
2012_02_02-PM-01_55_30
Home
Index