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
|
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 |
|
Leonardo de Moura
|
51a29098ab
|
fix: fixes #1852
|
2022-11-19 09:37:52 -08:00 |
|
Leonardo de Moura
|
22e96c71e9
|
fix: fixes #1850
|
2022-11-19 09:18:12 -08:00 |
|
Leonardo de Moura
|
a5ab59a413
|
fix: fixes #1851
|
2022-11-19 07:01:02 -08:00 |
|
Leonardo de Moura
|
5e9767a283
|
chore: fix test
|
2022-11-18 21:10:34 -08:00 |
|
Leonardo de Moura
|
556b6706ee
|
fix: fixes #1856
|
2022-11-18 19:34:32 -08:00 |
|
Leonardo de Moura
|
a7107aedb3
|
fix: fixes #1848
|
2022-11-18 08:49:10 -08:00 |
|
Mario Carneiro
|
f74fee07e6
|
doc: document Init.Data.List.Basic (#1828)
* doc: document Init.Data.List.Basic
* Apply suggestions from code review
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
|
2022-11-18 06:16:50 -08:00 |
|
Leonardo de Moura
|
d2a5ea137d
|
fix: fixes #1842
|
2022-11-16 17:29:41 -08:00 |
|
Leonardo de Moura
|
edadd8c034
|
fix: fixes #1841
This commit adds the configuration option
`ApplyConfig.approx` (available in Lean 3), and sets it to true by
default like in Lean 3.
|
2022-11-16 14:46:05 -08:00 |
|
Leonardo de Moura
|
7b03d9719c
|
fix: fixes #1679
|
2022-11-16 13:15:53 -08:00 |
|
Henrik Böving
|
e0d619e3ee
|
chore: basic tests for LCNF ElimDeadBranches
|
2022-11-16 08:17:13 -08:00 |
|
Leonardo de Moura
|
98922b878a
|
fix: fixes #1815
|
2022-11-15 17:08:54 -08:00 |
|