DeclSet ==
S:Id List
{i:Id| (i 
S)} 
x:Id fp-> Type
(i:{i:Id| (i S)} k:{k:Knd| 
hasloc(k;i)} fp-> Type)
Definitions :
list: type List,
product: x:A B[x],
function: x:A B[x],
l_member: (x l),
Id: Id,
fpf: a:A fp-> B[a],
set: {x:A| B[x]} ,
Knd: Knd,
assert: b,
hasloc: hasloc(k;i),
universe: Type
FDL editor aliases :
es-decl-set
DeclSet ==
S:Id List
\mtimes{} \{i:Id| (i \mmember{} S)\} {}\mrightarrow{} x:Id fp-> Type
\mtimes{} (i:\{i:Id| (i \mmember{} S)\} {}\mrightarrow{} k:\{k:Knd| \muparrow{}hasloc(k;i)\} fp-> Type)
Date html generated:
2010_08_27-AM-09_31_41
Last ObjectModification:
2009_12_16-AM-01_08_16
Home
Index