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.
32124 commits 1 branch 0 tags 5.3 GiB
Find a file
Kyle Miller c394a834c3
feat: extract delabAppCore, define withOverApp, and make over-applied projections pretty print (#3083) 
To handle delaborating notations that are functions that can be applied
to arguments, extracts the core function application delaborator as a
separate function that accepts the number of arguments to process and a
delaborator to apply to the "head" of the expression.

Defines `withOverApp`, which has the same interface as the combinator of
the same name from std4, but it uses this core function application
delaborator.

Uses `withOverApp` to improve a number of application delaborators,
notably projections. This means Mathlib can stop using `pp_dot` for
structure fields that have function types.

Incidentally fixes `getParamKinds` to specialize default values to use
supplied arguments, which impacts how default arguments are delaborated.

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2024-01-10 13:24:28 +00:00
.github chore: fix typo from #3148 in pr-release bot (#3154) 2024-01-10 03:14:43 +00:00
doc doc: avoid universe issue in example type class code (#3098) 2023-12-21 16:57:26 +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: extract delabAppCore, define withOverApp, and make over-applied projections pretty print (#3083) 2024-01-10 13:24:28 +00:00
stage0 chore: update stage0 2024-01-09 12:57:15 +01:00
tests feat: extract delabAppCore, define withOverApp, and make over-applied projections pretty print (#3083) 2024-01-10 13:24:28 +00:00
.gitattributes chore: Do not hide stage0/src/stdlib_flags.h from diffs 2023-09-13 19:29:25 +02:00
.gitignore chore: update tests to account for .lake 2023-11-13 20:31:24 -05:00
.ignore chore: ignore stage0/ (for rg etc.) 2022-03-18 15:28:20 +01:00
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 doc: setup 2021-01-03 13:21:58 +01:00
flake.lock chore: Nix bump to LLVM 15 2023-07-28 10:56:54 +02:00
flake.nix chore: Nix: use strings instead of URL literals (#2172) 2023-03-28 10:10:24 +02:00
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 chore: remove LICENSE header that confused GitHub 2021-11-18 09:42:35 +01:00
LICENSES chore: add GMP license for now 2021-11-18 09:42:35 +01:00
README.md doc: Update contribution guides (#2624) 2023-10-25 13:05:55 +11:00
RELEASES.md doc: add simproc release notes 2024-01-09 12:57:15 +01:00
shell.nix chore: Nix bump to LLVM 15 2023-07-28 10:56:54 +02:00

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.