max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
32041 commits 1 branch 0 tags 5.3 GiB
Find a file
Wojciech Nawrocki 2644b239a3
feat: snippet extension (#3054) 
# Summary

This makes a small addition to our take on the LSP protocol
in the form of supporting snippet text edits.
It has been discussed
[here](https://github.com/microsoft/language-server-protocol/issues/592)
on the LSP issue tracker for a while,
but seems unlikely to be added anytime soon.
This feature was requested by @PatrickMassot for the purposes
of supporting Lean code templates in code actions and widgets.

---------

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
2023-12-20 09:29:19 +00:00
.github chore: refine PR template (#3074) 2023-12-18 13:47:04 +00:00
doc fix: fixing path of the generated binary in documentation (#3093) 2023-12-19 17:26:55 +00:00
images
nix chore: set warningAsError in CI only (#3030) 2023-12-06 08:18:39 +00:00
script chore: refactor pr release workflow (#3020) 2023-12-12 00:45:10 +00:00
src feat: snippet extension (#3054) 2023-12-20 09:29:19 +00:00
stage0 feat: encode let_fun using a letFun function (#2973) 2023-12-18 09:01:42 +00:00
tests feat: add quot_precheck for expression tree elaborators (binop%, etc.) (#3078) 2023-12-18 16:52:49 +00:00
.gitattributes
.gitignore chore: update tests to account for .lake 2023-11-13 20:31:24 -05:00
.ignore
CMakeLists.txt feat: embed and check githash in .olean (#2766) 2023-11-27 10:24:43 +00:00
CODEOWNERS doc: widget code owner 2023-12-01 15:46:45 +00:00
CONTRIBUTING.md doc: Adjust contributor's docs to squash merging (#2927) 2023-11-21 10:13:43 +00:00
default.nix
flake.lock
flake.nix
lean-toolchain doc: VS Code dev setup (#2961) 2023-11-30 08:35:03 +00:00
lean.code-workspace chore: add the lean4 extension to the vscode workspace (#3059) 2023-12-14 08:58:21 +00:00
LICENSE
LICENSES
README.md doc: Update contribution guides (#2624) 2023-10-25 13:05:55 +11:00
RELEASES.md feat: snippet extension (#3054) 2023-12-20 09:29:19 +00:00
shell.nix

README.md

This is the repository for Lean 4.

We provide nightly releases and have just begun regular stable point releases.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.