Leonardo de Moura
|
83eaa47e0a
|
chore: move MatchEqs
|
2021-08-17 21:32:32 -07:00 |
|
Leonardo de Moura
|
a5b9306e04
|
fix: deep recursion at contradiction
|
2021-08-17 21:32:32 -07:00 |
|
Leonardo de Moura
|
52b52b22ef
|
fix: to do unfold matcher applications that cannot be reduced when smartUnfolding is true
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/How.20to.20WHNF.20without.20exposing.20recursors.3F
|
2021-08-17 21:32:32 -07:00 |
|
Jannis Limperg
|
9278e0694b
|
chore: add test case for BinomialHeap
|
2021-08-17 10:19:12 -07:00 |
|
Jannis Limperg
|
63628ef61b
|
fix: BinomialHeap: insert (head h) (tail h) = h
fixes #629
|
2021-08-17 10:19:12 -07:00 |
|
Leonardo de Moura
|
d775dc6195
|
feat: add flag for controlling the execution of initialize commands when importing modules programmatically
Fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Environment.20extensions.20in.20importModules
|
2021-08-16 17:43:28 -07:00 |
|
Leonardo de Moura
|
571a0491ee
|
feat: add Meta.byCases helper tactic
|
2021-08-16 14:58:51 -07:00 |
|
Leonardo de Moura
|
4fe65f3200
|
test: mathport issue https://github.com/dselsam/mathport/issues/18
|
2021-08-15 08:11:20 -07:00 |
|
Leonardo de Moura
|
9182ebd4c1
|
feat: elaborate * simp argument
|
2021-08-15 08:02:21 -07:00 |
|
Leonardo de Moura
|
3c68703f39
|
feat: elaborate <- modifier at simp arguments
|
2021-08-15 07:07:58 -07:00 |
|
Leonardo de Moura
|
4239ae69f6
|
chore: fix tests
|
2021-08-13 17:24:58 -07:00 |
|
Leonardo de Moura
|
d3d03df83c
|
feat: new elaborator for binop%
cc @gebner.
|
2021-08-13 15:44:59 -07:00 |
|
Sebastian Ullrich
|
d3f007b3cd
|
chore: fix stdlib benchmarks
|
2021-08-12 22:41:42 +02:00 |
|
Leonardo de Moura
|
da03262937
|
fix: check redundant sources at structure instance notation
|
2021-08-12 09:16:30 -07:00 |
|
Sebastian Ullrich
|
20accf5105
|
feat: revise macro parameter syntax
|
2021-08-12 07:48:42 -07:00 |
|
Leonardo de Moura
|
c68882ca67
|
feat: structure instance notation with multiple sources
closes #462
closes #463
|
2021-08-12 06:18:47 -07:00 |
|
Leonardo de Moura
|
a02a490a10
|
feat: add mkProjStx?
|
2021-08-12 05:41:00 -07:00 |
|
Daniel Selsam
|
5952a857cd
|
feat: pp.analyze improve heuristics for fun binders
|
2021-08-12 09:37:57 +02:00 |
|
Daniel Selsam
|
638d0ca8ed
|
feat: pp.instances and pp.instanceTypes
|
2021-08-12 09:33:30 +02:00 |
|
Daniel Selsam
|
040141f137
|
feat: unexpander for Subtype
|
2021-08-12 09:32:33 +02:00 |
|
Leonardo de Moura
|
74bd537465
|
fix: generation of to* field names
|
2021-08-11 17:25:02 -07:00 |
|
Leonardo de Moura
|
f1738ce2a0
|
feat: add macro for expanding field abbrev notation
The new macro allows us to use the field abbrev notation in patterns
too. See new test.
|
2021-08-11 16:02:50 -07:00 |
|
Daniel Selsam
|
efb3f528a6
|
fix: handle MData-wrapped app fns consistently in delaborator
Fixes #625
|
2021-08-11 18:53:32 +02:00 |
|
Leonardo de Moura
|
6352e549b5
|
test: add classes up to Field
|
2021-08-11 08:51:49 -07:00 |
|
Sebastian Ullrich
|
3b43ab47f1
|
fix: formatter: check for comment tokens
Fixes #624
|
2021-08-11 17:37:18 +02:00 |
|
Leonardo de Moura
|
d471f8df60
|
fix: fixes #621
|
2021-08-10 21:15:35 -07:00 |
|
Leonardo de Moura
|
61b3e6bcb8
|
fix: reduce projections of expanded structures at copyDefaultValue?
|
2021-08-10 20:50:59 -07:00 |
|
Leonardo de Moura
|
0623bb3860
|
feat: update fieldMap with composite field
|
2021-08-10 20:04:41 -07:00 |
|
Leonardo de Moura
|
ae03f15c92
|
test: default value set at copied structure
|
2021-08-10 19:00:34 -07:00 |
|
Leonardo de Moura
|
3b1285bee8
|
feat: process overriden default values in copied parents
|
2021-08-10 18:55:12 -07:00 |
|
Leonardo de Moura
|
295cae8afd
|
feat: copy field default values
Only basic examples are working. We still have many TODOs
|
2021-08-10 16:53:10 -07:00 |
|
Leonardo de Moura
|
47b8fa15f1
|
fix: propagate visibility annotation
|
2021-08-10 15:34:07 -07:00 |
|
Leonardo de Moura
|
16ea00586d
|
fix: fixes #620
|
2021-08-10 15:06:06 -07:00 |
|
Leonardo de Moura
|
972f00b0ff
|
fix: pending metavariable issue
It fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/let.20overload
|
2021-08-10 14:52:53 -07:00 |
|
Leonardo de Moura
|
b226ae738c
|
test: add CommGroup diamond
|
2021-08-10 10:20:37 -07:00 |
|
Leonardo de Moura
|
9cd729265e
|
fix: missing instantiateMVars
|
2021-08-10 10:04:16 -07:00 |
|
Leonardo de Moura
|
9fe1cd1026
|
chore: modify default value for option structureDiamondWarning
We still have some TODO items, but structure diamond support is
already useful in practice.
|
2021-08-10 09:24:53 -07:00 |
|
Leonardo de Moura
|
d03fa17c49
|
test: copyNewFieldsFrom
|
2021-08-10 09:19:27 -07:00 |
|
Leonardo de Moura
|
50deae9b8b
|
feat: copy binderInfo and inferMod from original field
|
2021-08-10 09:12:58 -07:00 |
|
Leonardo de Moura
|
bc26a9b527
|
feat: improve copyNewFieldsFrom
|
2021-08-10 09:08:35 -07:00 |
|
Leonardo de Moura
|
af1cecc641
|
feat: better error message
|
2021-08-10 07:46:15 -07:00 |
|
Leonardo de Moura
|
9e5998baf0
|
feat: register instance/reducible attribute for structuer diamond coercions
|
2021-08-10 07:16:59 -07:00 |
|
Leonardo de Moura
|
0f184a8c93
|
fix: binder annotation for class diamond coercions
|
2021-08-10 06:59:28 -07:00 |
|
Leonardo de Moura
|
2b71e16551
|
test: structure diamond coercion
|
2021-08-10 06:31:44 -07:00 |
|
Leonardo de Moura
|
bccad8edb1
|
feat: add coercion to parent structure whose fields having been copied
|
2021-08-09 19:01:08 -07:00 |
|
Leonardo de Moura
|
97664de3ee
|
fix: diamonds with dependent fields
|
2021-08-09 19:01:08 -07:00 |
|
Leonardo de Moura
|
e8403f89b0
|
fix: ensure field names are atomic
|
2021-08-09 19:01:08 -07:00 |
|
Leonardo de Moura
|
a0bd964255
|
test: overriding default value of private field
|
2021-08-09 19:01:08 -07:00 |
|
Leonardo de Moura
|
3f3e5d9dcb
|
fix: private field + default value bug
|
2021-08-09 19:01:08 -07:00 |
|
Leonardo de Moura
|
fdce7a99e1
|
feat: structure diamonds basic support
See TODO in the new comments.
|
2021-08-09 19:01:08 -07:00 |
|