Mario Carneiro 4f664fb3b5 feat: improve @[deprecated] attr (#3968) ... Complement to #3967 , adds a `(since := "<date>")` field to `@[deprecated]` so that metaprogramming code has access to the deprecation date for e.g. bulk removals. Also adds `@[deprecated "deprecation message"]` to optionally replace the default text "`{declName}` has been deprecated, use `{newName}` instead".		2024-04-23 17:00:32 +00:00
..
Certora2022	feat: improve @[deprecated] attr (#3968)	2024-04-23 17:00:32 +00:00
compiler	chore: move tests to new frontend	2020-10-23 14:07:26 -07:00
ICERM2022	feat: improve @[deprecated] attr (#3968)	2024-04-23 17:00:32 +00:00
NFM2022	feat: improve @[deprecated] attr (#3968)	2024-04-23 17:00:32 +00:00
bintree.lean	chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508)	2024-03-04 23:56:30 +00:00
bintree.lean.md	doc: embed examples into doc book	2022-04-06 09:06:49 -07:00
deBruijn.lean	chore: fix more typos in comments	2023-10-08 14:37:34 -07:00
deBruijn.lean.md	doc: embed examples into doc book	2022-04-06 09:06:49 -07:00
interp.lean	chore: fix more typos in comments	2023-10-08 14:37:34 -07:00
interp.lean.md	doc: embed examples into doc book	2022-04-06 09:06:49 -07:00
palindromes.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
palindromes.lean.md	doc: embed examples into doc book	2022-04-06 09:06:49 -07:00
phoas.lean	chore: fix more typos in comments	2023-10-08 14:37:34 -07:00
phoas.lean.md	doc: embed examples into doc book	2022-04-06 09:06:49 -07:00
tc.lean	chore: fix more typos in comments	2023-10-08 14:37:34 -07:00
tc.lean.md	doc: embed examples into doc book	2022-04-06 09:06:49 -07:00
test_single.sh	fix: unused variables linter review comments	2022-06-03 13:03:52 +02:00
widgets.lean	feat: bundle of widget improvements (#2964)	2023-12-21 06:24:33 +00:00
widgets.lean.md	chore: move tutorial to examples folder	2022-08-06 11:54:44 -07:00