5 commits

Author	SHA1	Message	Date
Jeremy Avigad	4050892889	refactor(library/*): rename 'compose' to 'comp'	2016-03-02 22:48:05 -05:00
Leonardo de Moura	deb1b3dc79	refactor(library): replace assert-exprs with have-exprs	2016-02-29 11:53:26 -08:00
Leonardo de Moura	d2eb99bf11	refactor(library/logic): move logic/choice.lean to init/classical.lean ... choice axiom is now in the classical namespace.	2015-08-12 18:37:33 -07:00
Leonardo de Moura	cb9830beaf	refactor(library/logic/choice): move prop_decidable instance into namespace 'classical'	2015-08-12 17:06:15 -07:00
Leonardo de Moura	bbd6946a15	refactor(library/logic/axioms): we have only one extra axiom	2015-07-29 13:36:23 -07:00

Renamed from library/logic/axioms/examples/leftinv_of_inj.lean (Browse further)