lean4-htt/src/frontends
Leonardo de Moura 55fee26b36 feat(library/class): add attribute for tracking symbols occurring in instances of type classes
For more information see:
https://github.com/leanprover/lean/wiki/Refactoring-structures
The new attribute [algebra] implements the [algebraic_class] described
in the page above.
2017-05-01 18:02:30 -07:00
..
lean feat(library/class): add attribute for tracking symbols occurring in instances of type classes 2017-05-01 18:02:30 -07:00
smt2 refactor(util/lean_path): explicitly pass around search path 2017-05-01 14:11:38 -07:00