Nuprl Definition : C_field_of
C_field_of(a;ctyp) == a ∈b map(λx.(fst(x));C_Struct-fields(ctyp)))
Definitions occuring in Statement :
C_Struct-fields: C_Struct-fields(v),
deq-member: x ∈b L),
atom-deq: AtomDeq,
map: map(f;as),
pi1: fst(t),
lambda: λx.A[x]
FDL editor aliases :
C_field_of
C\_field\_of(a;ctyp) == a \mmember{}\msubb{} map(\mlambda{}x.(fst(x));C\_Struct-fields(ctyp)))
Date html generated:
2015_07_17-AM-07_43_34
Last ObjectModification:
2011_09_29-PM-02_05_25
Home
Index