kevin/bat
1
0
Fork 0
mirror of https://github.com/sharkdp/bat synced 2026-08-26 14:13:37 +01:00
Code Issues Packages Projects Releases Wiki Activity
4,006 Commits 17 Branches 43 Tags
master
Commit Graph
5 Commits
This Branch
This Branch
All Branches
Author SHA1 Message Date
Y.D.X. 4661f22e81 Merge remote-tracking branch 'upstream/master' into lean 2025-07-11 13:03:06 +08:00
Y.D.X. (Gitpod) bfd8776042 chore: Follow Lean upstream 2025-07-11 12:56:46 +08:00
Y.D.X. 288b7e9ca3 docs: Add Lean/LICENSE.md 
> Jeremy Avigad:
> Patrick and I decided that it makes sense to release the text of MIL under CC BY 4.0 and the repository code (exercises, solutions, etc.) under Apache 2.0. We'll put the Apache license in the repo and figure out where to at the CC BY notice, but in the meantime, you can take this message as a declaration.

https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/License.20of.20Mathematics.20in.20Lean.3F/near/523527618
 2025-06-11 22:06:52 +08:00
Y.D.X. a9d5880dc8 docs: Update CHANGELOG, allow CC BY 4.0 license, and fix a markdown backquote 2025-06-10 17:44:10 +08:00
Y.D.X. 0918984249 Update Lean.sublime-syntax from Lean 3 to Lean 4 
Resolves #3286

1. `lean4.json` → `lean4.tmLanguage`

    1. Download `vscode-lean4/syntaxes/lean4.json` from https://github.com/leanprover/vscode-lean4/pull/623 (now merged).
    2. Install the VS Code extension [TextMate Languages (pedro-w)](https://marketplace.visualstudio.com/items?itemName=pedro-w.tmlanguage).
    3. Open `lean4.json` in VS Code, <kbd>F1</kbd>, and “Convert to tmLanguage PLIST File”.

2. `lean4.tmLanguage` → `lean4.sublime-syntax`

    Open `lean4.tmLanguage` in Sublime text, “Tools → Developer → New Syntax from lean4.tmLanguage…”.
 2025-06-10 17:41:33 +08:00