{ BaseDef 
' }
{ Proof }
Definitions occuring in Statement :
base-deriv: BaseDef,
member: t T,
universe: Type
Definitions :
equal: s = t,
member: t T,
bool: 
,
universe: Type,
limited-type: LimitedType,
set: {x:A| B[x]} ,
eclass: EClass(A[eo; e]),
function: x:A 
B[x],
all: 
x:A. B[x],
subtype_rel: A 
r B,
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
product: x:A 
B[x],
exists: 
x:A. B[x],
intensional-universe: IType,
isect: 
x:A. B[x],
b-union: A 
B,
union: left + right,
list: type List,
top: Top,
true: True,
fpf-cap: f(x)?z,
subtype: S T,
implies: P 
Q,
es-E-interface: E(X),
Id: Id,
name: Name,
base-deriv: BaseDef,
ldag: LabeledDAG(T),
tag-by: zT,
or: P 
Q,
rev_implies: P 
Q,
and: P 
Q,
iff: P Q,
labeled-graph: LabeledGraph(T),
record: record(x.T[x]),
isect2: T1 T2,
record+: record+,
fset: fset(T),
fpf-sub: f g,
deq: EqDecider(T),
ma-state: State(ds),
class-program: ClassProgram(T),
MaAuto: Error :MaAuto,
CollapseTHEN: Error :CollapseTHEN
Lemmas :
name_wf,
Id_wf,
intensional-universe_wf,
member_wf,
limited-type_wf,
subtype_rel_wf,
bool_wf
BaseDef \mmember{} \mBbbU{}'
Date html generated:
2010_08_27-PM-08_07_28
Last ObjectModification:
2010_06_18-AM-12_52_59
Home
Index