Leonardo de Moura 7c1cf9b6d3 chore: use extern lean_name_eq ... It uses pointer equality to improve performance. We will eventually be able to do it in Lean as soon as we re-activate the tactic framework.		2019-11-18 20:02:55 -08:00
..
Init	chore: use extern lean_name_eq	2019-11-18 20:02:55 -08:00
library.md	chore(library/library.md): update documentation	2017-08-16 14:17:26 -07:00
Makefile.in	chore: over-engineered build log	2019-11-13 19:01:49 +01:00
relative.py	chore: preparing for new naming convention	2019-10-04 14:22:23 -07:00