Sebastian Ullrich
d4caf1f922
fix: $_* anonymous suffix splice syntax pattern
2023-03-06 16:30:18 +01:00
Gabriel Ebner
0da281fab4
fix: reject occurrences of inductive type in index
...
Fixes #2125
2023-02-28 12:22:54 -08:00
Adrien Champion
473486eeb9
fix: calc indentation and allow underscore in first relation
2023-02-23 14:20:21 -08:00
Sebastian Ullrich
3f6c5f17db
fix: unhygiene in expandExplicitBinders
2023-02-22 17:07:31 +01:00
Gabriel Ebner
7992ce6b4d
chore: add test for calc
2023-02-21 16:41:46 -08:00
Gabriel Ebner
adcca17991
chore: add option to enable structure eta in tc search
2023-02-21 16:41:30 -08:00
Gabriel Ebner
75252d2b85
perf: whnf projections during defeq
2023-02-09 19:54:23 -08:00
Gabriel Ebner
448f49ee91
Revert "fix: reenable structure eta during tc search"
...
The fix is blocked by slow defeq checks for TC instances; see issues
1986 and 2055. Enabling it right now causes lots of timeouts in
mathlib4.
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/bump.20to.202023-02-06/near/326223768
This reverts commit 15a045ee66
2023-02-09 11:37:30 -08:00
Gabriel Ebner
3c562c1a9b
fix: unify goal before executing nested tactics in calc
...
Fixes #2095
2023-02-09 11:34:07 -08:00
Gabriel Ebner
15a045ee66
fix: reenable structure eta during tc search
...
Fixes #2074 .
2023-02-05 11:41:00 -08:00
Gabriel Ebner
d4b9a532d2
fix: calc: synthesize default instances
...
This is necessary to figure out the types with exponentiations.
Fixes #2079
2023-02-02 14:29:21 -08:00
Gabriel Ebner
8265d8bb13
chore: calc: improve error range
2023-02-02 14:21:06 -08:00
Gabriel Ebner
18b3bd7875
fix: calc: do not take lhs/rhs from expected type
...
Fixes #2073
2023-01-30 15:02:40 -08:00
Gabriel Ebner
e37f209c1a
fix: unify types in calc
2023-01-27 13:38:42 -08:00
Leonardo de Moura
decb08858f
fix: kernel must ensure that safe functions cannot use partial ones.
...
Fix issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Meaning.20of.20.60DefinitionSafety.2Epartial.60
2023-01-27 12:17:37 -08:00
Sebastian Ullrich
d01a521be2
test: fix
2023-01-26 13:31:16 +01:00
Sebastian Ullrich
badfcdc49f
fix: missing info tree on elab failure
2023-01-26 13:05:57 +01:00
Sebastian Ullrich
f24608c4d1
fix: make eoi an actual command with info tree
2023-01-26 13:05:57 +01:00
Sebastian Ullrich
8a4059dc65
fix: avoid notation in quotation elaborator output
2023-01-26 13:05:33 +01:00
Sebastian Ullrich
18297d8d91
fix: notation unexpander on overapplication of non-nullary notation
2023-01-26 13:05:33 +01:00
Rishikesh Vaishnav
561e404fe4
feat: make go-to-definition on a typeclass projection application go to the instance(s) ( #1767 )
2023-01-19 09:10:01 +00:00
Rishikesh Vaishnav
600758ba49
fix: fuzzy-find bonus for matching last characters of pattern and symbol ( #1917 )
2023-01-19 09:06:53 +01:00
Sebastian Ullrich
43c5ab802f
fix: show tactic info on canonical by
2023-01-18 10:23:37 +01:00
Sebastian Ullrich
223f1073d1
chore: info tree format should not leak hygiene IDs
2023-01-16 08:33:58 -08:00
Sebastian Ullrich
d59f5c2ffa
fix: binop% info tree
2023-01-16 08:33:58 -08:00
James Gallicchio
65db25bf49
feat: funext no arg tactic ( #2027 )
...
* feat: `funext` no arg tactic
Description of funext tactic includes behavior that is not implemented. This implements the behavior.
* fix
* feat: test new funext tactic
* use repeat for clarity of intent
2023-01-15 08:53:49 -08:00
Eric Wieser
8cd9ce0684
refactor: redefine Nat.mod such that rfl : 0 % n = 0
...
This property was true in Lean 3, and it was very convenient for working with `Fin n`.
2023-01-11 09:49:58 -08:00
James Gallicchio
37650f9147
fix: add done alternative to decreasing_with ( #2019 )
...
Previously `decreasing_with` failed if `simp_wf` closes the goal on its
own. This can cause undesired regressions when new `simp` lemmas are
introduced.
Closes #2018 .
2023-01-09 09:46:37 -08:00
Sebastian Ullrich
fff1e12878
fix: be more careful with MatchResult.uncovered in syntax match
2023-01-09 13:05:00 +01:00
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
