lean4-htt/doc/examples
Wojciech Nawrocki 8d04ac171d
feat: bundle of widget improvements (#2964)
Implements RFC #2963.

Leftover tasks:
- [x] Provide companion PR to vscode-lean4 (leanprover/vscode-lean4#376)
- [x] Companion PR to std4 (leanprover/std4#467)
- [x] Companion PR to ProofWidgets4
(leanprover-community/ProofWidgets4#36)
- [X] Companion commit to mathlib4
(0f4660f655)
- [ ] ~~Update the manual chapter~~ (will do in a follow-up)
2023-12-21 06:24:33 +00:00
..
Certora2022 doc: examples for Certora tutorial 2022-11-21 17:02:28 -08:00
compiler chore: move tests to new frontend 2020-10-23 14:07:26 -07:00
ICERM2022 chore: ICERM notation demo 2022-07-21 08:13:20 -04:00
NFM2022 doc: add slide headers to examples 2022-05-23 18:20:37 -07:00
bintree.lean chore: fix more typos in comments 2023-10-08 14:37:34 -07: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 chore: unused variables 2022-07-17 13:04:08 -04: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