71 Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5) |
71 Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5) |
72 "@SUM" :: "[idt,t,t] => t" ("(3\\<Sigma> _\\<in>_./ _)" 10) |
72 "@SUM" :: "[idt,t,t] => t" ("(3\\<Sigma> _\\<in>_./ _)" 10) |
73 "@PROD" :: "[idt,t,t] => t" ("(3\\<Pi> _\\<in>_./ _)" 10) |
73 "@PROD" :: "[idt,t,t] => t" ("(3\\<Pi> _\\<in>_./ _)" 10) |
74 "lam " :: "[idts, i] => i" ("(3\\<lambda>\\<lambda>_./ _)" 10) |
74 "lam " :: "[idts, i] => i" ("(3\\<lambda>\\<lambda>_./ _)" 10) |
75 |
75 |
|
76 syntax (HTML output) |
|
77 "@*" :: "[t,t]=>t" ("(_ \\<times>/ _)" [51,50] 50) |
|
78 Elem :: "[i, t]=>prop" ("(_ /\\<in> _)" [10,10] 5) |
|
79 Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5) |
|
80 "@SUM" :: "[idt,t,t] => t" ("(3\\<Sigma> _\\<in>_./ _)" 10) |
|
81 "@PROD" :: "[idt,t,t] => t" ("(3\\<Pi> _\\<in>_./ _)" 10) |
|
82 "lam " :: "[idts, i] => i" ("(3\\<lambda>\\<lambda>_./ _)" 10) |
|
83 |
76 rules |
84 rules |
77 |
85 |
78 (*Reduction: a weaker notion than equality; a hack for simplification. |
86 (*Reduction: a weaker notion than equality; a hack for simplification. |
79 Reduce[a,b] means either that a=b:A for some A or else that "a" and "b" |
87 Reduce[a,b] means either that a=b:A for some A or else that "a" and "b" |
80 are textually identical.*) |
88 are textually identical.*) |