Leonardo de Moura
474f1a4d39
feat: try to unify show type and expected type
...
The goal is to address the regression
```
example : (0 : Nat) + 0 = 0 :=
show 0 + 0 = 0 from rfl
```
introduced by fedf235cba
2023-01-06 08:48:48 -08:00
Leonardo de Moura
fedf235cba
fix: fixes #2011
...
In Lean 4, we have support for typing constraints of the form
```
(?m ...).1 =?= v
```
where the type of `?m ...` is a structure with a single field.
This kind of constraint is reduced to `?m ... =?= ⟨v⟩`
This feature is implemented by the function `isDefEqSingleton`.
As far as I remember, Lean 3 does not implement this feature.
This commit disables this feature if the structure is a class.
The goal is to avoid the generation of counterintuitive instances by
typing inference.
For example, in the example at issue #2011 , the following weird
instance was being generated for `Zero (f x)`
```
(@Zero.mk (f x✝) ((@instZero I (fun i => f i) fun i => inst✝¹ i).1 x✝)
```
where `inst✝¹` is the local instance `[∀ i, Zero (f i)]`
Note that this instance is definitinally equal to the expected nicer
instance `inst✝¹ x✝`.
However, the nasty instance trigger nasty unification higher order
constraints later.
Note that a few tests broke because different error messages were
produced. The new error messages seem better. I do not expect this
change to affect Mathlib4 since Lean 3 does not have this feature.
2023-01-05 17:33:45 -08:00
Leonardo de Moura
770815be9b
test: for issue #1937
2023-01-05 13:46:15 -08:00
Leonardo de Moura
9a236e70dc
fix: fixes #2009
2023-01-04 10:32:03 -08:00
Leonardo de Moura
6fea2946c2
fix: fixes #2006
2023-01-04 08:19:22 -08:00
Gabriel Ebner
181fbdfb42
feat: add fun x ↦ y syntax
2023-01-03 13:59:53 -08:00
Gabriel Ebner
70a6c06eef
fix: erase *dependent* local instances
2023-01-03 11:39:46 -08: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
