{ pi-example-inst() 
Pi_term }
{ Proof }
Definitions occuring in Statement :
pi-example-inst: pi-example-inst(),
pi_term: Pi_term,
member: t T
Definitions :
atom: Atom,
member: t T,
list: type List,
nil: [],
token: "$token",
cons: [car / cdr],
name: Name,
equal: s = t,
subtype: S 
T,
function: x:A 
B[x],
all: 
x:A. B[x],
eclass: EClass(A[eo; e]),
subtype_rel: A r B,
implies: P 
Q,
es-E-interface: E(X),
listp: A List
,
ndlist: ndlist(T),
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
tl: tl(l),
hd: hd(l),
pi-example: pi-example(x;y;z;v),
pi-example-inst: pi-example-inst(),
MaAuto: Error :MaAuto,
THEN: Error :THEN
Lemmas :
pi-example_wf,
subtype_rel_wf,
name_wf,
member_wf
pi-example-inst() \mmember{} Pi\_term
Date html generated:
2010_08_27-PM-08_40_01
Last ObjectModification:
2010_05_04-PM-05_11_04
Home
Index