{ SQType(Knd) }
{ Proof }
Definitions occuring in Statement :
Knd: Knd,
sq_type: SQType(T)
Definitions :
sq_type: SQType(T),
Knd: Knd,
all: 
x:A. B[x],
implies: P 
Q,
guard: {T},
member: t 
T,
so_lambda: 
x.t[x],
prop: 
,
btrue: tt,
assert: 
b,
ifthenelse: if b then t else f fi ,
true: True,
pi1: fst(t),
so_apply: x[s],
pi2: snd(t),
bfalse: ff,
false: False
Lemmas :
IdLnk_sq,
Id_sq,
pi1_wf,
IdLnk_wf,
pi2_wf,
Id_wf,
btrue_wf,
bfalse_wf,
assert_wf
SQType(Knd)
Date html generated:
2010_08_26-PM-11_32_33
Last ObjectModification:
2008_02_27-PM-09_22_42
Home
Index