lean4-htt/library
Sebastian Ullrich d0e53be0dd feat(library/init/lean/parser/parser_t): improve str's error message and allow error messages without 'unexpected' part
Showing the expected string at the initial position is much more helpful than
showing "unexpected <char>"
2018-07-05 10:20:25 +02:00
..
init feat(library/init/lean/parser/parser_t): improve str's error message and allow error messages without 'unexpected' part 2018-07-05 10:20:25 +02:00
system chore(*): remove more files 2018-05-21 06:42:58 -07:00
leanpkg.path feat(leanpkg): add package manager 2017-05-01 14:11:38 -07:00
library.md chore(library/library.md): update documentation 2017-08-16 14:17:26 -07:00