equal
deleted
inserted
replaced
44 "@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10) |
44 "@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10) |
45 "<*>" :: "[i, i] => i" (infixr 80) |
45 "<*>" :: "[i, i] => i" (infixr 80) |
46 |
46 |
47 translations |
47 translations |
48 "QSUM x:A. B" => "QSigma(A, %x. B)" |
48 "QSUM x:A. B" => "QSigma(A, %x. B)" |
49 "A <*> B" => "QSigma(A, _K(B))" |
49 "A <*> B" => "QSigma(A, %_. B)" |
50 |
50 |
51 constdefs |
51 constdefs |
52 qsum :: "[i,i]=>i" (infixr "<+>" 65) |
52 qsum :: "[i,i]=>i" (infixr "<+>" 65) |
53 "A <+> B == ({0} <*> A) Un ({1} <*> B)" |
53 "A <+> B == ({0} <*> A) Un ({1} <*> B)" |
54 |
54 |