Nuprl Definition : C_TYPE_eq_fun
C_TYPE_eq_fun(a) ==
C_TYPE_ind(a
Void=>λb.C_Void?(b)
Int=>λb.C_Int?(b)
Struct(fields)=>rec.λb.(C_Struct?(b)
∧b (||fields|| =z ||C_Struct-fields(b)||)
∧b (∀i∈upto(||fields||).fst(fields[i]) =a fst(C_Struct-fields(b)[i])
∧b (rec i (snd(C_Struct-fields(b)[i]))))_b)
Array(length,elems)=>rec.λb.(C_Array?(b) ∧b (length =z C_Array-length(b)) ∧b (rec C_Array-elems(b)))
Pointer(to)=>rec.λb.(C_Pointer?(b) ∧b (rec C_Pointer-to(b))))
Definitions occuring in Statement :
C_TYPE_ind: C_TYPE_ind,
C_Pointer-to: C_Pointer-to(v),
C_Pointer?: C_Pointer?(v),
C_Array-elems: C_Array-elems(v),
C_Array-length: C_Array-length(v),
C_Array?: C_Array?(v),
C_Struct-fields: C_Struct-fields(v),
C_Struct?: C_Struct?(v),
C_Int?: C_Int?(v),
C_Void?: C_Void?(v),
bl-all: (∀x∈L.P[x])_b,
upto: upto(n),
select: L[n],
length: ||as||,
band: p ∧b q,
eq_atom: x =a y,
eq_int: (i =z j),
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
C_TYPE_eq_fun
C\_TYPE\_eq\_fun(a) ==
C\_TYPE\_ind(a
Void=>\mlambda{}b.C\_Void?(b)
Int=>\mlambda{}b.C\_Int?(b)
Struct(fields)=>rec.\mlambda{}b.(C\_Struct?(b)
\mwedge{}\msubb{} (||fields|| =\msubz{} ||C\_Struct-fields(b)||)
\mwedge{}\msubb{} (\mforall{}i\mmember{}upto(||fields||).fst(fields[i]) =a fst(C\_Struct-fields(b)[i])
\mwedge{}\msubb{} (rec i (snd(C\_Struct-fields(b)[i]))))\_b)
Array(length,elems)=>rec.\mlambda{}b.(C\_Array?(b)
\mwedge{}\msubb{} (length =\msubz{} C\_Array-length(b))
\mwedge{}\msubb{} (rec C\_Array-elems(b)))
Pointer(to)=>rec.\mlambda{}b.(C\_Pointer?(b) \mwedge{}\msubb{} (rec C\_Pointer-to(b))))
Date html generated:
2015_07_17-AM-07_42_43
Last ObjectModification:
2014_06_08-PM-08_01_40
Home
Index