Sebastian Ullrich
|
de180e5c7a
|
fix: private + pp.fullNames
|
2022-12-21 21:59:05 +01:00 |
|
Sebastian Ullrich
|
eaafd36918
|
feat: use signature pretty printer in #check id/#check @id
|
2022-12-21 21:59:05 +01:00 |
|
Sebastian Ullrich
|
b6bd2dea35
|
feat: signature pretty printer for hovers
|
2022-12-21 21:59:05 +01:00 |
|
Sebastian Ullrich
|
533c770e36
|
refactor: remove redundant state
|
2022-12-21 21:59:05 +01:00 |
|
Gabriel Ebner
|
572ffe77e3
|
fix: implement assertAfter using revert
|
2022-12-21 21:42:07 +01:00 |
|
Gabriel Ebner
|
eeab2af7ae
|
fix: remove Inhabited Environment instance
|
2022-12-21 20:08:08 +01:00 |
|
Gabriel Ebner
|
443c1a08e5
|
fix: lsp change debouncing
|
2022-12-21 20:02:53 +01:00 |
|
Gabriel Ebner
|
586079462c
|
doc: explain variable conditions in type classes
|
2022-12-21 04:24:39 +01:00 |
|
Gabriel Ebner
|
14f8ff1642
|
feat: add CoeOut class
|
2022-12-21 04:24:39 +01:00 |
|
Gabriel Ebner
|
c7fb3a1c91
|
chore: make use of CoeHead chaining
|
2022-12-21 04:24:39 +01:00 |
|
Gabriel Ebner
|
78676a5a5a
|
refactor: chain CoeHead
|
2022-12-21 04:24:39 +01:00 |
|
Gabriel Ebner
|
2b97392f2e
|
refactor: use @[coe_decl] attribute
|
2022-12-21 04:24:39 +01:00 |
|
Gabriel Ebner
|
e59ddb0c16
|
refactor: replace hardcoded list of coercions by attribute
|
2022-12-21 04:24:39 +01:00 |
|
Gabriel Ebner
|
d2203aa5a0
|
chore: restrict dangerous typed syntax coercions
|
2022-12-21 04:24:39 +01:00 |
|
Gabriel Ebner
|
118567657d
|
chore: remove dangerous instances in json-rpc
|
2022-12-21 04:24:39 +01:00 |
|
Gabriel Ebner
|
434d889f4d
|
chore: remove dangerous instances
|
2022-12-21 04:24:39 +01:00 |
|
Gabriel Ebner
|
54290d537b
|
fix: deterministic fvar alias printing
|
2022-12-21 03:08:18 +01:00 |
|
Sebastian Ullrich
|
96ccf192e8
|
fix: parenthesize by optParam values
|
2022-12-20 18:10:39 +01:00 |
|
Gabriel Ebner
|
e386d5941e
|
refactor: replace ignoreLevelMVarDepth by levelAssignDepth
|
2022-12-19 20:14:17 +01:00 |
|
Mario Carneiro
|
8b0699cd3b
|
fix: disable memoize in pattern conv
|
2022-12-19 06:21:54 -08:00 |
|
Sebastian Ullrich
|
f732afed0a
|
fix: dynamic linking of Lean programs
|
2022-12-18 12:19:21 +01:00 |
|
Scott Morrison
|
7c29cc742b
|
chore: add iff_self to simpOnlyBuiltins
|
2022-12-15 01:00:30 +01:00 |
|
Sebastian Ullrich
|
d5fb32a393
|
fix: hygiened goal tags in conv congr
|
2022-12-14 16:36:47 +01:00 |
|
locriacyber
|
fa761b8baf
|
chore: fix typo in CLI usage (--ldlags) (#1947)
|
2022-12-14 10:20:50 +01:00 |
|
Sebastian Ullrich
|
636afc654a
|
fix: avoid mapping .oleans in the way of the stack
|
2022-12-13 22:11:41 +01:00 |
|
Sebastian Ullrich
|
3cebe7464c
|
fix: protect against jumping over the stack guard page
|
2022-12-13 22:02:05 +01:00 |
|
Sebastian Ullrich
|
88c8cd5cf2
|
fix: show correct goal state after an empty by
|
2022-12-13 01:39:45 +01:00 |
|
Sebastian Ullrich
|
9c9cc017df
|
fix: ignore empty character literals
|
2022-12-12 22:59:06 +01:00 |
|
Gabriel Ebner
|
f3f4eba945
|
fix: make Format.*join* tail-recursive
|
2022-12-12 22:58:21 +01:00 |
|
Gabriel Ebner
|
1c8ef51124
|
fix: make List.toString tail-recursive
|
2022-12-12 22:58:21 +01:00 |
|
Mario Carneiro
|
eb3b0377d7
|
fix: List.groupBy
|
2022-12-12 16:55:27 +01:00 |
|
Wojciech Nawrocki
|
a9ba08ce11
|
doc: document msgToInteractiveDiagnostic
|
2022-12-07 19:16:25 +01:00 |
|
Sebastian Ullrich
|
6169435259
|
refactor: consolidate MessageData constructors into lazy formatting with infos
|
2022-12-07 19:16:25 +01:00 |
|
Gabriel Ebner
|
4b87103931
|
chore: ignore document version errors
|
2022-12-03 01:20:47 +01:00 |
|
tydeu
|
fe09c9c824
|
chore: update Lake
|
2022-12-03 01:19:29 +01:00 |
|
ChrisHughes24
|
e168806078
|
chore: rename Prod.ext
|
2022-12-02 20:24:19 +01:00 |
|
Leonardo de Moura
|
8a573b5d87
|
fix: fixes #1900
|
2022-12-02 10:04:01 -08:00 |
|
Leonardo de Moura
|
a999015371
|
feat: add applicationTime to registerTagAttribute
|
2022-12-02 09:58:41 -08:00 |
|
Leonardo de Moura
|
50fc4a6ad8
|
fix: fixes #1907
|
2022-12-02 08:59:16 -08:00 |
|
Gabriel Ebner
|
681bbe5cf4
|
feat: ByteArray.hash
|
2022-12-01 20:18:14 -08:00 |
|
Gabriel Ebner
|
9b416667e7
|
chore: replace all hashes by murmurhash
|
2022-12-01 20:18:14 -08:00 |
|
Gabriel Ebner
|
b0cadbc1fa
|
fix: support escaped field names in deriving FromJson/ToJson
|
2022-12-02 03:48:19 +01:00 |
|
Gabriel Ebner
|
3d1571896c
|
fix: support escaped field names in dot-notation
|
2022-12-02 03:48:19 +01:00 |
|
Gabriel Ebner
|
7af80766e3
|
fix: do not ignore applicationTime in parametric attributes
|
2022-12-02 02:15:35 +01:00 |
|
Leonardo de Moura
|
ffb0f42aae
|
fix: fixes #1901
|
2022-12-01 08:39:06 -08:00 |
|
Leonardo de Moura
|
0dda3a8c02
|
fix: include instance implicits that depend on outParams at outParamsPos
This fixes the fix for #1852
|
2022-12-01 06:11:48 -08:00 |
|
Leonardo de Moura
|
0a031fc9bb
|
chore: replace Expr.forEach with Expr.forEachWhere
|
2022-12-01 05:19:32 -08:00 |
|
Sebastian Ullrich
|
af5efe0b2d
|
doc: MonadReader
|
2022-12-01 10:16:04 +01:00 |
|
Leonardo de Moura
|
30d625697e
|
chore: use Expr.forEachWhere to implement linter
closes #1899
TODO: use `Expr.forEachWhere` in other modules. There are many other opportunities.
|
2022-11-30 18:44:20 -08:00 |
|
Leonardo de Moura
|
1c5706bcc0
|
feat: add Expr.forEachWhere
|
2022-11-30 18:41:12 -08:00 |
|