Austin Letson

Syntax for creating concrete HashMaps

2

In reviewing documentation examples for HashMap, @digama0 [mentioned that it would be nice to have syntax for constructing concrete HashMaps](https://github.com/leanprover/std4/pull/725#discussion_r1558731044). The proposed syntax is `{"one" ↦ 2, "two" ↦ 2}`...

`lean-action` template for `lake new/init`

1

### Proposal Add a template to `lake new/init` to allow users to automatically include a default continuous integration workflow that uses [lean-action](https://github.com/leanprover/lean-action). With the `auto-config` improvement introduced by leanprover/lean-action#61, a...

feat: detect default target on runLinter

6

Now `runLinter` will try to detect all root modules of the default build targets of type `lean_exe` or `lean_lib` in Lake's environment using the same `resolveDefaultPackageTarget` function as `lake build`....

refactor: use lean-action in makefile.yml CI workflow

2

### Description: `lean-action` now supports the macOS runner so you can now use it in makefile.yml ### License: By submitting this pull request, I confirm that my contribution is made...