Nuprl Definition : es-decl-set
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 occuring in Statement :
fpf: a:A fp-> B[a],
hasloc: hasloc(k;i),
Knd: Knd,
Id: Id,
l_member: (x ∈ l),
list: T List,
assert: ↑b,
set: {x:A| B[x]} ,
function: x:A ─→ B[x],
product: x:A × B[x],
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:
2015_07_17-AM-11_55_05
Last ObjectModification:
2013_03_27-AM-10_38_09
Home
Index