Sebastian Ullrich
|
87e860f871
|
perf: Array.push: move elements directly when source is unique
|
2021-12-16 06:37:37 -08:00 |
|
tydeu
|
72cfe18e9f
|
chore: update Lake
|
2021-12-16 11:10:33 +01:00 |
|
Joe Hendrix
|
5a307a93ac
|
fix: bug at ByteArray.copySlice
|
2021-12-16 11:05:19 +01:00 |
|
Leonardo de Moura
|
fa8b015603
|
chore: update stage0
|
2021-12-15 17:09:39 -08:00 |
|
Leonardo de Moura
|
81f7335269
|
fix: ensure motive is type correct at simpProj
|
2021-12-15 17:07:31 -08:00 |
|
Leonardo de Moura
|
0a81093db5
|
fix: bug at simpProj
This bug was reported at https://github.com/dwrensha/lean4-maze/issues/1
|
2021-12-15 17:07:00 -08:00 |
|
Leonardo de Moura
|
9a24db4e86
|
fix: check generated motives at ▸ notation
This commit also improves the `▸` notation a bit.
It now tries `subst` (if applicable) before failing.
|
2021-12-15 16:16:42 -08:00 |
|
Leonardo de Moura
|
89edc184fb
|
feat: compleation at #print command
|
2021-12-15 13:13:39 -08:00 |
|
Leonardo de Moura
|
653b684651
|
feat: improve getCompletionKindForDecl
|
2021-12-15 12:57:09 -08:00 |
|
Leonardo de Moura
|
7d7c6d8be5
|
feat: add CompletionItemKind
|
2021-12-15 11:24:11 -08:00 |
|
Leonardo de Moura
|
31f845c5ed
|
feat: keyword completion
|
2021-12-15 11:24:11 -08:00 |
|
Leonardo de Moura
|
043e9c80b4
|
feat: add Trie.findPrefix
|
2021-12-15 11:24:11 -08:00 |
|
Sebastian Ullrich
|
ba83721109
|
chore: add comment for previous fix
|
2021-12-15 20:10:48 +01:00 |
|
Sebastian Ullrich
|
35e623fca0
|
chore: update stage0
|
2021-12-15 15:58:32 +01:00 |
|
Sebastian Ullrich
|
c8c39aa4bb
|
chore: lean-gdb: fix RC printing
|
2021-12-15 15:58:31 +01:00 |
|
Sebastian Ullrich
|
3c9ea3b113
|
fix: wait on tasks before Lean program exit
|
2021-12-15 15:58:24 +01:00 |
|
larsk21
|
efa2ded224
|
chore: bump server version to 0.1.1
|
2021-12-15 13:00:05 +01:00 |
|
larsk21
|
d50c08360d
|
feat: change error flag to progress kind in LeanFileProgressProcessingInfo
|
2021-12-15 13:00:05 +01:00 |
|
larsk21
|
dcbc526115
|
feat: report header processing errors as error progress
|
2021-12-15 13:00:05 +01:00 |
|
larsk21
|
925c530673
|
feat: add error field to LeanFileProgressProcessingInfo
|
2021-12-15 13:00:05 +01:00 |
|
Siddharth
|
37982c6d5c
|
doc: structure update
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
|
2021-12-15 11:48:46 +00:00 |
|
Gabriel Ebner
|
230d6d2cf5
|
fix: use group for if-then-else
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
202fd1414a
|
chore: update stage0
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
d6f629860b
|
feat: add ppRealFill and ppRealGroup combinators
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
b905824024
|
chore: fix tests
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
ab3e08190b
|
feat: allow opt-out of grouping in formatter
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
b6efece612
|
fix: missing space after /--
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
4f81972996
|
fix: missing newline before inductionAlt
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
f1fc8f2441
|
fix: space before where/:= in inductive
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
7be0d7ec16
|
fix: space before $
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
3f73442a5a
|
fix: space before infer modifiers
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
b176efefca
|
fix: print line before deriving
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
5d25df1a69
|
fix: indenting of match arms in declValEqns
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
067c181075
|
fix: space after @&
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
e1b2c945e3
|
fix: suppress extra spaces in formatter
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
2b7ec7f9ef
|
fix: spacing around (← monadic lifts)
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
52b36cad1d
|
fix: whitespace around parens in open/export
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
87faa7a93a
|
fix: whitespace after rw/simp [<-
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
f219188c95
|
fix: indent declaration signatures
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
e90bdd00db
|
fix: indent where definitions and add space before
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
f5a2562575
|
fix: indent structure fields
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
316fa81042
|
fix: print spaces around <| and |>
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
f1d583c9cf
|
fix: newline in whereDecls
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
448d2cd951
|
feat: add script to reformat lean files
|
2021-12-15 11:42:38 +00:00 |
|
Gabriel Ebner
|
7e483d3a0a
|
feat: support syntax abbreviations in dynamic quotations
|
2021-12-15 11:17:58 +00:00 |
|
tydeu
|
a3250dc44b
|
feat: expose --load-dynlib functionality to Lean code
|
2021-12-15 08:26:48 +00:00 |
|
Leonardo de Moura
|
34430cd7c3
|
fix: semantic highlighting for keywords of the form #<alpha>...
closes #703
|
2021-12-14 17:58:56 -08:00 |
|
Leonardo de Moura
|
5b14caf329
|
fix: missing addTermInfo at elabAtomicDiscr
closes #820
|
2021-12-14 17:20:46 -08:00 |
|
tydeu
|
42d8c333a6
|
chore: update Lake
|
2021-12-14 14:36:21 -08:00 |
|
Gabriel Ebner
|
45bcef5dab
|
refactor: server: use String.firstDiffPos to find changes
This is necessary so that we do not reprocess the whole file if
incremental sync is disabled.
|
2021-12-14 11:55:34 -08:00 |
|