Leonardo de Moura
44e889bd52
chore: avoid runtime bounds check
2022-10-27 07:48:30 -07:00
Leonardo de Moura
0a35ce7e3e
perf: add ModuleData.constNames
2022-10-27 07:34:07 -07:00
Leonardo de Moura
95689d914f
perf: use NameHashSet instead of NameSet
2022-10-27 07:10:54 -07:00
Leonardo de Moura
2c4056c104
chore: use exit during finalization
...
Motivation: Lean startup time profiling.
2022-10-27 06:51:29 -07:00
Leonardo de Moura
23ba495205
perf: better initial const2ModIdx size
2022-10-26 22:22:41 -07:00
Leonardo de Moura
39249f0c1d
perf: zero startup time function summaries
2022-10-26 21:55:37 -07:00
Leonardo de Moura
ad98df80fe
feat: congr theorems using Iff
...
closes #1763
2022-10-26 18:00:24 -07:00
Leonardo de Moura
5e25d9148a
feat: improve apply error message when root term elaboration is postponed
...
fixes #1719
2022-10-26 17:15:24 -07:00
Leonardo de Moura
0b6b754bca
feat: improve apply tactic
...
It tries to address what the Mathlib community calls the "apply bug".
cc @digama0
2022-10-26 16:58:43 -07:00
Leonardo de Moura
f3b1eadb55
feat: copy docstring when copying parent fields
...
closes #1730
2022-10-26 15:43:46 -07:00
Leonardo de Moura
83d8e36773
fix: fixes #1780
2022-10-26 07:46:38 -07:00
Leonardo de Moura
5a8f9ace72
fix: open .. hinding .. should activate scoped attributes
2022-10-26 07:39:06 -07:00
Leonardo de Moura
e369c3beb6
fix: disallow . immediately after ..
...
Rejects the following weird example
```
```
which was being parsed as
```
```
2022-10-26 07:13:40 -07:00
Leonardo de Moura
d7e732e886
feat: use unop% to implement unary minus notation
...
closes #1779
2022-10-26 06:55:24 -07:00
Leonardo de Moura
1216f5e658
feat: support for unop% at CollectPatternVars
2022-10-26 06:51:14 -07:00
Leonardo de Moura
e6caee97ec
feat: unop% elaborator
...
We now have support for unary operators at `Op.toTree` and `Op.toExpr`
see #1779
2022-10-26 06:44:44 -07:00
Leonardo de Moura
00ca0dde5c
feat: add unop% term parser
...
We not to support unary minus at `BinOp.toTree`
see #1779
2022-10-26 06:19:22 -07:00
Mario Carneiro
a086d217a5
fix: bug in level normalization (soundness bug)
2022-10-26 05:22:26 -07:00
Sebastian Ullrich
1893857f15
fix: expandCDot? should create canonical syntax
2022-10-25 12:23:13 +02:00
Sebastian Ullrich
f39281f6b4
fix: hoverableInfoAt? in presence of canonical syntax
2022-10-25 12:23:13 +02:00
Sebastian Ullrich
36fbf53a79
chore: improve trace.Elab.info formatting
2022-10-25 12:23:13 +02:00
Leonardo de Moura
e55badef05
feat: List.mapMono
2022-10-24 19:50:09 -07:00
Leonardo de Moura
2cd21e08ba
chore: add CollectLevelParams.visitLevels
2022-10-24 19:50:09 -07:00
Leonardo de Moura
81f8ab8fbb
refactor: Level.instantiateParams => Level.substParams, add Level.instantiateParams
...
Motivation: make sure `Level.instantiateParams` and
`Expr.instantiateLevelParams` have similar types.
2022-10-24 19:49:57 -07:00
Mario Carneiro
d7d61bfb55
feat: use withoutPosition consistently (part 2)
2022-10-24 12:51:32 -07:00
Mario Carneiro
765ebcdbf0
feat: use withoutPosition consistently
2022-10-24 12:51:32 -07:00
Gabriel Ebner
4ff6798284
perf: use instantiation cache
2022-10-24 12:23:13 -07:00
Gabriel Ebner
fa9538ffa6
perf: use old instantiateLevelParams in compiler
2022-10-24 12:23:13 -07:00
Gabriel Ebner
d87c36157a
perf: speed up Expr.replace
2022-10-24 12:23:13 -07:00
Gabriel Ebner
dcc97c9bbe
fix: preserve sharing in instantiateLevelParams
2022-10-24 12:23:13 -07:00
Gabriel Ebner
725aa8b39a
refactor: instantiateTypeLevelParams in Lean
2022-10-24 12:23:13 -07:00
Mario Carneiro
e7c7678ab0
refactor: line wrapping in parser code
2022-10-24 08:37:29 -07:00
David Renshaw
e4ab10dc30
doc: fix some typos
...
assinged -> assigned
collction -> collection
2022-10-24 16:01:39 +02:00
mcdoll
6cf9a63193
doc: fix typo ( #1775 )
...
equaal -> equal
2022-10-24 15:05:51 +02:00
Sebastian Ullrich
3a12c99666
chore: register Elab.app trace classes
2022-10-24 13:16:36 +02:00
Yuri de Wit
c98b3a5388
fix: add local Hashable instance ( fixes #1737 )
...
When inductives are indirectly mutually recursive, say `inductive T | t
(args: List T)` instead of `inductive T | t (arg : T)`, Lean would fail
to find an instance of Hashable for `T` because it was not yet defined.
This commit makes sure that the deriving handler adds a needed Hashable T
instance to the local scope so that Hashable.hash can be resolved
recursively.
2022-10-23 21:26:04 +02:00
Mario Carneiro
c4cbefce11
feat: add linter.deprecated option to silence deprecation warnings
2022-10-23 21:11:57 +02:00
Mario Carneiro
b3ba78aade
feat: hovers & name resolution in registerCombinatorAttribute (part 2)
2022-10-23 09:30:38 +02:00
Mario Carneiro
f168af76a7
feat: hovers & name resolution in registerCombinatorAttribute
2022-10-23 09:30:38 +02:00
David Renshaw
16320a297f
doc: fix some typos
...
Leah -> Lean
giveName -> givenName
2022-10-22 21:16:35 +02:00
Henrik Böving
1e00eff3e7
fix: jp context extender missed out on some variables
2022-10-21 17:58:47 -07:00
Henrik Böving
dac6127810
feat: Compiler pass for reducing common jp args
2022-10-21 17:35:40 -07:00
Henrik Böving
a608532fd4
chore: Improve LCNF check goto error message
2022-10-21 17:35:40 -07:00
Gabriel Ebner
fc304d95c0
feat: Min/Max typeclasses
2022-10-21 14:36:38 -07:00
Gabriel Ebner
041307fd4b
fix: build
2022-10-20 12:42:32 -07:00
E.W.Ayers
46112a5f2a
fix: review
2022-10-20 11:20:42 -07:00
E.W.Ayers
c9a26596dc
refactor: switch resolve to double eval strategy
...
Using option (2) from this comment:
https://github.com/leanprover/lean4/pull/1661#pullrequestreview-1135363727
2022-10-20 11:20:42 -07:00
E.W.Ayers
691835037e
feat: code action resolvers
2022-10-20 11:20:42 -07:00
E.W.Ayers
297d06fc0c
fix: issue where code action was not running
2022-10-20 11:20:42 -07:00
E.W.Ayers
c795e2b073
fix: rm CodeActionData
2022-10-20 11:20:42 -07:00
