Skip to content

Commit a3cf551

Browse files
Lean 4 VS Code Extensionalexjgreig
Lean 4 VS Code Extension
authored and
alexjgreig
committed
Initial commit
1 parent 87f303a commit a3cf551

File tree

8 files changed

+131
-0
lines changed

8 files changed

+131
-0
lines changed

‎.github/workflows/lean_action_ci.yml

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
name: Lean Action CI
2+
3+
on:
4+
push:
5+
pull_request:
6+
workflow_dispatch:
7+
8+
jobs:
9+
build:
10+
runs-on: ubuntu-latest
11+
12+
steps:
13+
- uses: actions/checkout@v4
14+
- uses: leanprover/lean-action@v1

‎.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
/.lake

‎Quave.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
-- This module serves as the root of the `Quave` library.
2+
-- Import modules here that should be built as part of the library.
3+
import Quave.Basic

‎Quave/Basic.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
def hello := "world"

‎README.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
# Quave

‎lake-manifest.json

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
{"version": "1.1.0",
2+
"packagesDir": ".lake/packages",
3+
"packages":
4+
[{"url": "https://github.com/leanprover-community/mathlib4",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "leanprover-community",
8+
"rev": "d677d774e4dc693f6e6b8ed518c093154a7188fa",
9+
"name": "mathlib",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "master",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/leanprover-community/plausible",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "leanprover-community",
18+
"rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
19+
"name": "plausible",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "v4.16.0-rc1",
22+
"inherited": true,
23+
"configFile": "lakefile.toml"},
24+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
25+
"type": "git",
26+
"subDir": null,
27+
"scope": "leanprover-community",
28+
"rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
29+
"name": "LeanSearchClient",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": "main",
32+
"inherited": true,
33+
"configFile": "lakefile.toml"},
34+
{"url": "https://github.com/leanprover-community/import-graph",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "leanprover-community",
38+
"rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
39+
"name": "importGraph",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "main",
42+
"inherited": true,
43+
"configFile": "lakefile.toml"},
44+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "leanprover-community",
48+
"rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
49+
"name": "proofwidgets",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "v0.0.50",
52+
"inherited": true,
53+
"configFile": "lakefile.lean"},
54+
{"url": "https://github.com/leanprover-community/aesop",
55+
"type": "git",
56+
"subDir": null,
57+
"scope": "leanprover-community",
58+
"rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
59+
"name": "aesop",
60+
"manifestFile": "lake-manifest.json",
61+
"inputRev": "v4.16.0-rc1",
62+
"inherited": true,
63+
"configFile": "lakefile.toml"},
64+
{"url": "https://github.com/leanprover-community/quote4",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "leanprover-community",
68+
"rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
69+
"name": "Qq",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "v4.15.0",
72+
"inherited": true,
73+
"configFile": "lakefile.toml"},
74+
{"url": "https://github.com/leanprover-community/batteries",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "c104265c34eb8181af14e8dbc14c2f034292cb02",
79+
"name": "batteries",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "main",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover/lean4-cli",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover",
88+
"rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
89+
"name": "Cli",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "main",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"}],
94+
"name": "Quave",
95+
"lakeDir": ".lake"}

‎lakefile.toml

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
name = "Quave"
2+
version = "0.1.0"
3+
keywords = ["math"]
4+
defaultTargets = ["Quave"]
5+
6+
[leanOptions]
7+
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
8+
autoImplicit = false
9+
10+
[[require]]
11+
name = "mathlib"
12+
scope = "leanprover-community"
13+
14+
[[lean_lib]]
15+
name = "Quave"

‎lean-toolchain

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
leanprover/lean4:v4.16.0-rc2

0 commit comments

Comments
 (0)