Siddharth
|
b6eb780144
|
feat: LLVM backend (#1837)
|
2022-12-30 12:45:30 +01:00 |
|
Gabriel Ebner
|
d19033e443
|
fix: correctly parse json unicode escapes
|
2022-12-23 17:04:10 -08:00 |
|
Gabriel Ebner
|
430d7d05d6
|
feat: add derive handler for Nonempty
|
2022-12-22 03:48:15 +01:00 |
|
Gabriel Ebner
|
a90afa8a51
|
fix: tests
|
2022-12-22 02:02:55 +01:00 |
|
Gabriel Ebner
|
e71a2e58bb
|
fix: remove misleading leading space in " where"
|
2022-12-21 22:54:42 +01:00 |
|
Gabriel Ebner
|
0d598dcfdf
|
fix: Format.align always prints whitespace
|
2022-12-21 22:54:42 +01:00 |
|
Sebastian Ullrich
|
de9a6374f1
|
feat: make #check <ident> always show the signature without elaboration
|
2022-12-21 21:59:05 +01:00 |
|
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
|
84de976111
|
chore: fix copy-produced script
|
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 |
|
Gabriel Ebner
|
572ffe77e3
|
fix: implement assertAfter using revert
|
2022-12-21 21:42:07 +01:00 |
|
Gabriel Ebner
|
78676a5a5a
|
refactor: chain CoeHead
|
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
|
2606021304
|
fix: use ppTerm instead of formatTerm
|
2022-12-21 03:08:18 +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 |
|
Scott Morrison
|
7c29cc742b
|
chore: add iff_self to simpOnlyBuiltins
|
2022-12-15 01:00:30 +01:00 |
|
Mario Carneiro
|
52d00e8944
|
test: macro scopes in Conv.congr (#1955)
|
2022-12-14 16:43:26 +00:00 |
|
Sebastian Ullrich
|
88c8cd5cf2
|
fix: show correct goal state after an empty by
|
2022-12-13 01:39:45 +01:00 |
|
Gabriel Ebner
|
1c8ef51124
|
fix: make List.toString tail-recursive
|
2022-12-12 22:58:21 +01:00 |
|
Leonardo de Moura
|
8a573b5d87
|
fix: fixes #1900
|
2022-12-02 10:04:01 -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
|
a67a5080e9
|
chore: fix tests after hash change
|
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 |
|
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 |
|
Sebastian Ullrich
|
50b2ad89b4
|
test: limit maxRecDepth
|
2022-12-01 10:06:57 +01:00 |
|
Leonardo de Moura
|
5a151ca64c
|
chore: fix tests
|
2022-11-30 17:52:37 -08:00 |
|
Leonardo de Moura
|
3e45060dd5
|
fix: disable implicit lambdas for local variables without type information
Problem reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/why.20doesn't.20this.20unify.3F/near/312806870
|
2022-11-29 14:33:16 -08:00 |
|
Leonardo de Moura
|
069873d8e5
|
fix: fixes #1891
|
2022-11-29 08:59:46 -08:00 |
|
Mario Carneiro
|
40e212c166
|
feat: infer def/theorem DefKind for let rec
|
2022-11-29 08:16:47 -08:00 |
|
Gabriel Ebner
|
6e23ced6d9
|
fix: test
|
2022-11-29 08:16:09 -08:00 |
|
Gabriel Ebner
|
bdbab653fd
|
fix: synthesize tc instances before propagating expected type
|
2022-11-29 08:16:09 -08:00 |
|
Henrik Böving
|
5286c2b5aa
|
feat: optimize mul/div into shift operations
|
2022-11-29 01:05:06 +01:00 |
|
Mario Carneiro
|
17ef0cea8a
|
feat: intra-line withPosition formatting
|
2022-11-28 09:02:08 -08:00 |
|
Leonardo de Moura
|
c510d16ef5
|
fix: fixes #1808
|
2022-11-28 07:48:54 -08:00 |
|
Leonardo de Moura
|
36cc7c23b6
|
fix: fixes #1886
|
2022-11-28 06:50:44 -08:00 |
|
Sebastian Ullrich
|
42a080fae2
|
fix: comments ending in --/
Fixes #1883
|
2022-11-25 10:32:49 +01:00 |
|
Sebastian Ullrich
|
39f2322f35
|
fix: save correct environment in info tree for example
|
2022-11-24 13:11:14 -08:00 |
|
Leonardo de Moura
|
543a7e26d4
|
test: for #1878
closes #1878
|
2022-11-24 13:03:45 -08:00 |
|
Leonardo de Moura
|
c53c5b5e16
|
fix: fixes #1882
Better support for `intro <type-ascription>`.
It was treating it as a pattern before this commit.
|
2022-11-24 12:40:25 -08:00 |
|
Leonardo de Moura
|
9d8b324f8d
|
fix: fixes #1869
Better support for simplifying class projections.
|
2022-11-24 11:56:36 -08:00 |
|
Leonardo de Moura
|
1ec535d523
|
test: alternative encoding experiment for decEq and noConfusion
|
2022-11-23 18:46:10 -08:00 |
|
Leonardo de Moura
|
0694731af8
|
fix: fixes #1870
|
2022-11-23 05:49:19 -08:00 |
|
Sebastian Ullrich
|
019707ccf4
|
fix: do method lifting across choice nodes
|
2022-11-21 17:52:14 +01:00 |
|