4 commits

Author	SHA1	Message	Date
Leonardo de Moura	ced742083a	feat(library/init/quot): add helper function quot.rec_on_subsingleton₂	2015-04-01 13:04:41 -07:00
Leonardo de Moura	ed1acd9fb0	feat(library/init): move propext to init/quot, add Jeremy's funext theorem	2015-04-01 12:36:33 -07:00
Leonardo de Moura	0da4f191fc	feat(library/init/quot): add rec_on for subsingleton types	2015-04-01 11:57:39 -07:00
Leonardo de Moura	b960e123b1	feat(kernel): add experimental support for quotient types	2015-03-31 22:04:16 -07:00