Mario Carneiro
118d1027d2
feat: go to definition for KeyedDeclsAttributes
2022-11-16 11:16:24 +01:00
Mario Carneiro
583e023314
chore: snake-case attributes (part 2)
2022-10-19 09:28:08 -07:00
Mario Carneiro
dd5948d641
chore: snake-case attributes (part 1)
2022-10-19 09:28:08 -07:00
Mario Carneiro
4c1ed9e2bc
fix: hovers in appUnexpander attr
2022-10-14 10:06:12 +02:00
Gabriel Ebner
45c4f2faa0
refactor: remove _aux_discr
2022-10-11 17:24:35 -07:00
Ed Ayers
2a6697e077
feat: goal-diffs ( #1610 )
2022-09-24 11:46:11 +02:00
Mario Carneiro
6392c5b456
chore: import reductions
2022-09-15 14:02:38 -07:00
Gabriel Ebner
a6a913495d
feat: make (_ : a = b) hoverable in infoview
2022-08-25 18:38:21 +02:00
Sebastian Ullrich
5160cb7b0f
refactor: remove some unnecessary antiquotation kind annotations
2022-07-23 17:09:32 +02:00
Gabriel Ebner
a8cab84735
refactor: use computed fields for Expr
2022-07-11 14:19:41 -07:00
Leonardo de Moura
2446c64a99
chore: cleanup
2022-07-04 07:15:04 -07:00
Sebastian Ullrich
22475b8669
refactor: introduce common TSyntax abbreviations
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
a78302243c
refactor: strengthen Syntax signatures
...
Most notable change: `Quote` is now parameterized by the target kind.
Which means that `Name` etc. could actually have different
implementations for quoting into `term` and `level`, if that need ever
arises.
2022-06-27 22:37:02 +02:00
Leonardo de Moura
f6d1e48cb8
fix: constant => opaque issues
2022-06-14 17:19:54 -07:00
Leonardo de Moura
041827bed5
chore: unused variables
2022-06-07 17:54:10 -07:00
E.W.Ayers
1785ab142e
refactor: move Lean.PrettyPrinter.Delaborator.SubExpr to Lean.SubExpr
...
This is because SubExpr has uses outside the Delaborator.
Closes #1183
2022-06-03 12:38:14 -07:00
Wojciech Nawrocki
9c9407e722
feat: propagate tagAppFns in delaborator
2022-05-31 00:07:56 +02:00
Leonardo de Moura
3cf425ba52
fix: pattern hover information
...
We annotate patterns with the corresponding `Syntax` during
elaboration, and do not populate the info tree. Reason: the set of
pattern variables is not known during pattern elaboration.
2022-04-08 15:03:42 -07:00
Leonardo de Moura
37b321229f
feat: make sure hover information does not include @ for constants
2022-04-07 18:40:04 -07:00
Leonardo de Moura
55989c25fc
chore: remove unnecessary args
2022-04-07 18:19:15 -07:00
Leonardo de Moura
46ce3013d0
feat: cleanup local context before elaborating match alternatives RHS
2022-03-29 18:52:07 -07:00
Leonardo de Moura
3862e7867b
refactor: make String.Pos opaque
...
TODO: this refactoring exposed bugs in `FuzzyMatching` and `Lake`
closes #410
2022-03-20 10:47:13 -07:00
Leonardo de Moura
90c442da76
feat: add internal option for communicating to the delaborator that input term is a pattern
2022-03-16 07:50:29 -07:00
Leonardo de Moura
12e2a79170
chore: fix codebase after removing auto pure
2022-02-03 18:08:14 -08:00
Leonardo de Moura
bac91b9b5b
chore: remove arbitrary
2022-01-15 12:14:27 -08:00
Gabriel Ebner
bdc80ce50d
fix: potential nontermination in delabFor
2022-01-12 09:41:41 +01:00
Gabriel Ebner
5aab241f7a
fix: show correct popup for a + b
2021-10-26 20:19:27 +02:00
Gabriel Ebner
bfc74decde
feat: add info field to Syntax.node
2021-10-26 20:19:27 +02:00
Leonardo de Moura
fb27537b8e
fix: appUnexpander name resolution
...
fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Scoping.20for.20delaborator.3F
2021-10-09 08:29:26 -07:00
Leonardo de Moura
3714cf16ec
refactor: lazy evaluation for <|>
...
see #617
2021-09-07 17:06:10 -07:00
Leonardo de Moura
f4ecbd1102
chore: reduce dependencies
2021-08-24 17:38:43 -07:00
Wojciech Nawrocki
81eff794d5
doc: add review comments
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
fd016c6065
chore: address some comments
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
1bab9f6ffc
refactor: simplify delaborator monad stacks
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
73363bef1f
fix: delab structure field annotations
2021-08-24 08:57:41 -07:00
Daniel Selsam
2f484ec096
feat: build info trees in delab
2021-08-24 08:57:41 -07:00
Leonardo de Moura
3293e9ef08
chore: fix module comments, they must occur after the imports
2021-08-06 14:02:42 -07:00
Daniel Selsam
652681621a
fix: pp.analyze don't type-annotate mdatas
2021-08-03 09:13:18 +02:00
Daniel Selsam
ea6fca24c2
refactor: pp.analyze StateT for analyzeApp
2021-08-03 09:13:18 +02:00
Daniel Selsam
44f1f4e410
refactor: pp.analyze needs pp options
2021-08-03 09:13:18 +02:00
Daniel Selsam
48d5c0d2a6
chore: pp.proofs defaults to false
2021-08-03 09:13:18 +02:00
Daniel Selsam
702211db2a
feat: pp.analyze detect when struct-inst type needed
2021-08-03 09:13:18 +02:00
Daniel Selsam
1f183cdc30
fix: only pp.analyze when all is not set
2021-08-03 09:13:18 +02:00
Daniel Selsam
54146f1859
fix: 4-ary SubExpr repr for types
2021-08-03 09:13:18 +02:00
Daniel Selsam
aa590ccdf5
feat: pp option to instantiate mvars
2021-08-03 09:13:18 +02:00
Daniel Selsam
50d67e77ac
fix: type ascriptions
2021-08-03 09:13:18 +02:00
Daniel Selsam
811bb56d10
fix: never set a negation
2021-08-03 09:13:18 +02:00
Daniel Selsam
89364b802b
feat: top-down heuristic delaboration
2021-08-03 09:13:18 +02:00
Wojciech Nawrocki
f51b80060d
feat: generic tagged Format
2021-08-01 09:58:44 +02:00
Leonardo de Moura
f4a7ffd8c8
chore: fix codebase and tests
2021-06-29 17:14:52 -07:00
